Variance and covariance of uniform averages

Over a finite type, the covariance 𝔼 (f - 𝔼 f) (g - 𝔼 g) of two real functions under the uniform distribution is 𝔼 f g - 𝔼 f 𝔼 g (Fintype.expect_sub_expect_mul_sub_expect), and so the variance 𝔼 (f - 𝔼 f) ^ 2 is 𝔼 f ^ 2 - (𝔼 f) ^ 2 (Fintype.expect_sub_expect_sq) O'Donnell, Propositions 1.13 and 1.16. Like the rest of the library, these write the variance and covariance inline rather than through a named definition.

Main results

• Fintype.expect_sub_expect_mul_sub_expect: the covariance is 𝔼 f g - 𝔼 f 𝔼 g.
• Fintype.expect_sub_expect_sq: the variance is 𝔼 f ^ 2 - (𝔼 f) ^ 2.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Fintype.expect_sub_expect_mul_sub_expect {α : Type u_1} [Fintype α] (f g : α → ℝ) : (Finset.univ.expect fun (x : α) => (f x - Finset.univ.expect fun (y : α) => f y) * (g x - Finset.univ.expect fun (y : α) => g y)) = (Finset.univ.expect fun (x : α) => f x * g x) - (Finset.univ.expect fun (x : α) => f x) * Finset.univ.expect fun (x : α) => g x

The covariance of uniform averages is the average of the product minus the product of the averages O'Donnell, Proposition 1.16.

theorem Fintype.expect_sub_expect_sq {α : Type u_1} [Fintype α] (f : α → ℝ) : (Finset.univ.expect fun (x : α) => (f x - Finset.univ.expect fun (y : α) => f y) ^ 2) = (Finset.univ.expect fun (x : α) => f x ^ 2) - (Finset.univ.expect fun (x : α) => f x) ^ 2

The variance of a uniform average is the average of the square minus the square of the average O'Donnell, Proposition 1.13.