Uniform averages of indicators and second moments

Over a finite type, the uniform average of the indicator of a predicate is the density of the set where it holds (Fintype.expect_boole), the counterpart for 𝔼 of Finset.sum_boole: the probability of an event under the uniform distribution is the expectation of its indicator. With it, Markov's inequality bounds the density of the set where a nonnegative function is large by its average (Fintype.mul_dens_filter_le_expect), and the second moment method bounds the density of the set where a function does not vanish from below by the square of its average over the average of its square (Fintype.sq_expect_le_dens_mul_expect_sq).

The square of an average is at most the average of the squares (Finset.sq_expect_le_expect_sq), the form for 𝔼 of sum_div_card_sq_le_sum_sq_div_card; both inequalities of second moments are cases of the Cauchy–Schwarz inequality Finset.expect_mul_sq_le_sq_mul_sq, which also gives its form with square roots (Real.expect_mul_le_sqrt_mul_sqrt, the form for 𝔼 of Real.sum_mul_le_sqrt_mul_sqrt) and the triangle inequality for √(𝔼 f²) (Fintype.expect_add_sq_le).

The uniform average over a product is the iterated average (Fintype.expect_prod_type), so a function of some of the coordinates has the same average on the product (Fintype.expect_comp_fst, Fintype.expect_comp_snd), and a function on a product splits orthogonally into its fiber averages and a part of average zero on every fiber (Fintype.exists_eq_add_expect_fiber_eq_zero). The uniform average on a finite group is translation invariant (Fintype.expect_add_left), and resampling one coordinate of a uniformly random tuple leaves its average unchanged (Fintype.expect_expect_update).

Main results

• Finset.sq_expect_le_expect_sq: the square of an average is at most the average of the squares.
• Finset.prod_filter_mem_eq_prod_filter_notMem: the sets containing an element are the sets avoiding it, with the element inserted.
• Real.expect_mul_le_sqrt_mul_sqrt: the Cauchy–Schwarz inequality for averages.
• Fintype.expect_prod_type, Fin.expect_univ_cons: the average over a product or non-empty tuple type is the iterated average.
• Fintype.expect_comp_fst, Fintype.expect_comp_snd, Fintype.expect_comp_fst_snd_fst: a function of some of the coordinates has the same average on the product.
• Fintype.expect_unique, Fintype.expect_bool: averages on Unique types and Bool.
• Fintype.expect_add_left, Fintype.expect_expect_update, Fintype.expect_comp_arrowCongr, Fintype.expect_sumElim, Fintype.expect_restrict_coordinates: translation, coordinate-resampling, coordinate-renaming, disjoint-union splitting, and coordinate-restriction invariance of uniform averages.
• Fintype.expect_sub_expect_fiber, Fintype.expect_add_sq_of_expect_fiber_eq_zero, Fintype.exists_eq_add_expect_fiber_eq_zero: orthogonal fiber decomposition of second moments on product types.
• Fintype.expect_boole: the average of an indicator is a density.
• Fintype.mul_dens_filter_le_expect: Markov's inequality for a uniform average.
• Fintype.sq_expect_le_dens_mul_expect_sq: the second moment method for a uniform average.
• Fintype.expect_add_sq_le, Fintype.expect_sq_le_of_expect_mul_le: second-moment bounds from triangle and Cauchy–Schwarz inequalities.

theorem Finset.sq_expect_le_expect_sq {ι : Type u_1} {R : Type u_2} [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] [Module ℚ≥0 R] [PosSMulMono ℚ≥0 R] (s : Finset ι) (f : ι → R) : (s.expect fun (i : ι) => f i) ^ 2 ≤ s.expect fun (i : ι) => f i ^ 2

The square of an average is at most the average of the squares.

theorem Finset.prod_filter_mem_eq_prod_filter_notMem {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (g : Finset ι → M) : ∏ S : Finset ι with i ∈ S, g S = ∏ T : Finset ι with i ∉ T, g (insert i T)

The sets containing i are the sets avoiding i, with i inserted.

theorem Finset.sum_filter_mem_eq_sum_filter_notMem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (g : Finset ι → M) : ∑ S : Finset ι with i ∈ S, g S = ∑ T : Finset ι with i ∉ T, g (insert i T)

The sets containing i are the sets avoiding i, with i inserted.

theorem Real.expect_mul_le_sqrt_mul_sqrt {ι : Type u_1} (s : Finset ι) (f g : ι → ℝ) : (s.expect fun (i : ι) => f i * g i) ≤ √(s.expect fun (i : ι) => f i ^ 2) * √(s.expect fun (i : ι) => g i ^ 2)

The Cauchy–Schwarz inequality for averages, with square roots.

theorem Fintype.expect_prod_type {α : Type u_3} {β : Type u_4} {M : Type u_6} [Fintype α] [Fintype β] [AddCommMonoid M] [Module ℚ≥0 M] (f : α × β → M) : (Finset.univ.expect fun (x : α × β) => f x) = Finset.univ.expect fun (a : α) => Finset.univ.expect fun (b : β) => f (a, b)

The uniform average over a product is the iterated average.

theorem Fintype.expect_comp_fst {α : Type u_3} {β : Type u_4} {M : Type u_6} [Fintype α] [Fintype β] [AddCommMonoid M] [Module ℚ≥0 M] [Nonempty β] (f : α → M) : (Finset.univ.expect fun (p : α × β) => f p.1) = Finset.univ.expect fun (a : α) => f a

A function of the first coordinate has the same average on the product.

theorem Fintype.expect_comp_snd {α : Type u_3} {β : Type u_4} {M : Type u_6} [Fintype α] [Fintype β] [AddCommMonoid M] [Module ℚ≥0 M] [Nonempty α] (f : β → M) : (Finset.univ.expect fun (p : α × β) => f p.2) = Finset.univ.expect fun (b : β) => f b

A function of the second coordinate has the same average on the product.

theorem Fintype.expect_comp_fst_snd_fst {α : Type u_3} {β : Type u_4} {γ : Type u_5} {M : Type u_6} [Fintype α] [Fintype β] [Fintype γ] [AddCommMonoid M] [Module ℚ≥0 M] [Nonempty γ] (f : α × β → M) : (Finset.univ.expect fun (p : α × β × γ) => f (p.1, p.2.1)) = Finset.univ.expect fun (q : α × β) => f q

A function of the first two coordinates has the same average on the product of three.

theorem Fintype.expect_add_left {M : Type u_6} [AddCommMonoid M] [Module ℚ≥0 M] {G : Type u_7} [AddGroup G] [Fintype G] (f : G → M) (x : G) : (Finset.univ.expect fun (y : G) => f (x + y)) = Finset.univ.expect fun (y : G) => f y

Translation invariance: adding a fixed element permutes a finite additive group, so the uniform average is unchanged.

theorem Fintype.expect_unique {α : Type u_3} {M : Type u_6} [Fintype α] [AddCommMonoid M] [Module ℚ≥0 M] [Unique α] (f : α → M) : (Finset.univ.expect fun (a : α) => f a) = f default

The uniform average over a type with a unique element is the value at default.

theorem Fintype.expect_expect_update {ι : Type u_1} [Fintype ι] {α : Type u_3} {M : Type u_6} [Fintype α] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] [Nonempty α] (F : (ι → α) → M) (i : ι) : (Finset.univ.expect fun (s : ι → α) => Finset.univ.expect fun (a : α) => F (Function.update s i a)) = Finset.univ.expect fun (s : ι → α) => F s

Resampling one coordinate of a uniformly random function keeps it uniformly random.

theorem Fintype.expect_comp_arrowCongr {ι : Type u_1} [Fintype ι] {α : Type u_3} {M : Type u_6} [Fintype α] [AddCommMonoid M] [Module ℚ≥0 M] {κ : Type u_7} [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (h : (κ → α) → M) : (Finset.univ.expect fun (x : ι → α) => h fun (j : κ) => x (e.symm j)) = Finset.univ.expect fun (y : κ → α) => h y

Renaming the coordinates preserves uniform averages over function types.

theorem Fintype.expect_sumElim {ι : Type u_1} [Fintype ι] {α : Type u_3} {M : Type u_6} [Fintype α] [AddCommMonoid M] [Module ℚ≥0 M] {κ : Type u_7} [Fintype κ] [DecidableEq ι] [DecidableEq κ] (h : (ι ⊕ κ → α) → M) : (Finset.univ.expect fun (x : ι ⊕ κ → α) => h x) = Finset.univ.expect fun (x₁ : ι → α) => Finset.univ.expect fun (x₂ : κ → α) => h (Sum.elim x₁ x₂)

The uniform average on functions out of ι ⊕ κ is the iterated average over functions on ι and functions on κ.

theorem Fintype.expect_restrict_coordinates {ι : Type u_1} [Fintype ι] {α : Type u_3} {M : Type u_6} [Fintype α] [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] [Nonempty α] {p : ι → Prop} [DecidablePred p] (f : ({ i : ι // p i } → α) → M) : (Finset.univ.expect fun (x : ι → α) => f fun (i : { i : ι // p i }) => x ↑i) = Finset.univ.expect fun (x : { i : ι // p i } → α) => f x

Restricting a uniformly random function on ι to a subtype of coordinates gives a uniformly random function on the subtype.

theorem Fintype.expect_bool {𝕜 : Type u_2} [Semifield 𝕜] [CharZero 𝕜] (f : Bool → 𝕜) : (Finset.univ.expect fun (b : Bool) => f b) = (f false + f true) / 2

The uniform average on Bool is the midpoint of the two values.

theorem Fintype.expect_sub_expect_fiber {α : Type u_3} {β : Type u_4} {M : Type u_5} [Fintype β] [AddCommGroup M] [Module ℚ≥0 M] (f : α × β → M) (a : α) : (Finset.univ.expect fun (b : β) => f (a, b) - Finset.univ.expect fun (b' : β) => f (a, b')) = 0

Subtracting from a function its averages over the fibers {a} × β leaves averages zero over the fibers.

theorem Fintype.expect_add_sq_of_expect_fiber_eq_zero {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (φ : α → ℝ) {g : α × β → ℝ} (hg : ∀ (a : α), (Finset.univ.expect fun (b : β) => g (a, b)) = 0) : (Finset.univ.expect fun (p : α × β) => (φ p.1 + g p) ^ 2) = (Finset.univ.expect fun (p : α × β) => φ p.1 ^ 2) + Finset.univ.expect fun (p : α × β) => g p ^ 2

Pythagoras' theorem for the splitting of a function on α × β into a function of the first coordinate and a function of average zero over every fiber {a} × β.

theorem Fintype.exists_eq_add_expect_fiber_eq_zero {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] [Nonempty β] (f : α × β → ℝ) : ∃ (f₁ : α → ℝ) (f₂ : α × β → ℝ), (f = fun (p : α × β) => f₁ p.1 + f₂ p) ∧ (∀ (a : α), (Finset.univ.expect fun (b : β) => f₂ (a, b)) = 0) ∧ ((Finset.univ.expect fun (a : α) => f₁ a) = Finset.univ.expect fun (p : α × β) => f p) ∧ (Finset.univ.expect fun (p : α × β) => f p ^ 2) = (Finset.univ.expect fun (a : α) => f₁ a ^ 2) + Finset.univ.expect fun (p : α × β) => f₂ p ^ 2

Every function on α × β is a function of the first coordinate, its averages over the fibers {a} × β, plus a function of average zero over every fiber, and the second moments add up.

theorem Fintype.expect_sq_le_of_expect_mul_le {ι : Type u_1} [Fintype ι] {u w : ι → ℝ} {c : ℝ} (h : (Finset.univ.expect fun (i : ι) => u i * u i) ≤ c * (√(Finset.univ.expect fun (i : ι) => u i ^ 2) * √(Finset.univ.expect fun (i : ι) => w i ^ 2))) : (Finset.univ.expect fun (i : ι) => u i ^ 2) ≤ c ^ 2 * Finset.univ.expect fun (i : ι) => w i ^ 2

If 𝔼 u² ≤ c √(𝔼 u²) √(𝔼 w²) then 𝔼 u² ≤ c² 𝔼 w².

theorem Fintype.expect_boole {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [Semifield 𝕜] [CharZero 𝕜] (p : ι → Prop) [DecidablePred p] : (Finset.univ.expect fun (i : ι) => if p i then 1 else 0) = ↑{i : ι | p i}.dens

The uniform average of the indicator of p is the density of the set where p holds.

theorem Fintype.mul_dens_filter_le_expect {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : ι → 𝕜} (hf : ∀ (i : ι), 0 ≤ f i) (a : 𝕜) : a * ↑{i : ι | a ≤ f i}.dens ≤ Finset.univ.expect fun (i : ι) => f i

Markov's inequality for a uniform average: a nonnegative function is at least a on a set of density at most its average divided by a.

theorem Fintype.sq_expect_le_dens_mul_expect_sq {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] (f : ι → 𝕜) : (Finset.univ.expect fun (i : ι) => f i) ^ 2 ≤ ↑{i : ι | f i ≠ 0}.dens * Finset.univ.expect fun (i : ι) => f i ^ 2

The second moment method for a uniform average: the square of the average of f is at most the density of the set where f does not vanish times the average of f ^ 2. So f does not vanish on a set of density at least (𝔼 f) ^ 2 / 𝔼 f ^ 2.

theorem Fintype.expect_expect_one_sub_le {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {β : Type u_3} [Nonempty ι] [Fintype β] [Nonempty β] {c : ι → β → 𝕜} {δ : 𝕜} (h : ∀ (i : ι), 1 - δ ≤ Finset.univ.expect fun (j : β) => c i j) : (Finset.univ.expect fun (i : ι) => Finset.univ.expect fun (j : β) => 1 - c i j) ≤ δ

A read that is correct with probability at least 1 - δ whatever the first argument is wrong with probability at most δ on average.

theorem Fintype.expect_add_sq_le {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {X Y : ι → 𝕜} {a b α β A : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hA : 0 ≤ A) (hX : (Finset.univ.expect fun (i : ι) => X i ^ 2) ≤ α ^ 2 * A) (hY : (Finset.univ.expect fun (i : ι) => Y i ^ 2) ≤ β ^ 2 * A) : (Finset.univ.expect fun (i : ι) => (a * X i + b * Y i) ^ 2) ≤ (a * α + b * β) ^ 2 * A

The triangle inequality for √(𝔼 f²), squared: if 𝔼 X² ≤ α² A and 𝔼 Y² ≤ β² A, then 𝔼 (a X + b Y)² ≤ (a α + b β)² A for a, b ≥ 0.

theorem Fin.expect_univ_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Fintype (α i)] {M : Type u_2} [AddCommMonoid M] [Module ℚ≥0 M] (f : ((i : Fin (n + 1)) → α i) → M) : (Finset.univ.expect fun (x : (i : Fin (n + 1)) → α i) => f x) = Finset.univ.expect fun (a : α 0) => Finset.univ.expect fun (y : (i : Fin n) → α i.succ) => f (cons a y)

Splitting off the first coordinate of a tuple on Fin (n + 1): the uniform average over (i : Fin (n + 1)) → α i is the iterated average over the head α 0 and the tail.