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,Fin.sum_univ_cons_bool,Fin.expect_univ_cons_bool: the average or sum over a product or non-empty tuple type is the iterated average or sum.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,Fintype.expect_unique_bool: averages onUniquetypes andBool.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,Fintype.expect_boole_sq,Fintype.expect_boole_mem,Fintype.expect_boole_mem_sq: the average of an indicator (or its square) 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.
The square of an average is at most the average of the squares.
The sets containing i are the sets avoiding i, with i inserted.
The sets containing i are the sets avoiding i, with i inserted.
The uniform average over a product is the iterated average.
A function of the first coordinate has the same average on the product.
A function of the second coordinate has the same average on the product.
Translation invariance: adding a fixed element permutes a finite additive group, so the uniform average is unchanged.
The uniform average over a type with a unique element is the value at default.
Resampling one coordinate of a uniformly random function keeps it uniformly random.
Renaming the coordinates preserves uniform averages over function types.
The uniform average on functions out of ι ⊕ κ is the iterated average over functions on ι
and functions on κ.
Restricting a uniformly random function on ι to a subtype of coordinates gives a uniformly
random function on the subtype.
Subtracting from a function its averages over the fibers {a} × β leaves averages zero over
the fibers.
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} × β.
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.
If 𝔼 u² ≤ c √(𝔼 u²) √(𝔼 w²) then 𝔼 u² ≤ c² 𝔼 w².
An indicator function is its own square, so the average of its square is the density of the set where the predicate holds.
The uniform average of the squared indicator of membership in S is the density of S.
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.
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.
A read that is correct with probability at least 1 - δ whatever the first argument is wrong
with probability at most δ on average.
The triangle inequality for √(𝔼 f²), squared: if 𝔼 X² ≤ α² A and 𝔼 Y² ≤ β² A, then
𝔼 (a X + b Y)² ≤ (a α + b β)² A for a, b ≥ 0.
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.
Splitting off the first bit of a tuple on Fin (n + 1): the sum over Fin (n + 1) → Bool
is the sum with first bit false plus the sum with first bit true.