Second moments of sample means

Let X₁, …, X_r be pairwise independent, square-integrable random vectors in a real Hilbert space with a common mean m. Their sample mean S = r⁻¹ ∑ₖ Xₖ has mean-square error

∫ ‖S - m‖² dP = r⁻² ∑ₖ ∫ ‖Xₖ - m‖² dP,

so that averaging r samples with a common per-sample error γ divides it by r. Together with Chebyshev's inequality for the second moment, TauCeti.meas_ge_le_integral_norm_sq_div_sq in TauCeti.Probability.Moments.Chebyshev, this is the scale 1 / r behind the elementary concentration of empirical moments.

The identity rests on Bienaymé's identity for random vectors: the squared norm of a sum of pairwise independent, centered, square-integrable random vectors has expectation equal to the sum of the expected squared norms. Only pairwise independence is used, through the factorization ∫ ⟪Xᵢ, Xⱼ⟫ = ⟪∫ Xᵢ, ∫ Xⱼ⟫ of ProbabilityTheory.IndepFun.integral_bilin, which makes every cross term vanish. The sample mean is TauCeti.finiteMean, and the scalar statement is the case E = ℝ.

Main statements

• TauCeti.integral_norm_sum_sq_of_pairwise_integral_inner_eq_zero: the second-moment identity for pairwise orthogonal random vectors with integrable pairwise inner products.
• TauCeti.integral_norm_sum_sq_of_pairwise_indepFun: Bienaymé's identity for random vectors.
• TauCeti.integral_norm_finiteMean_sub_sq: the mean-square error of a sample mean.
• TauCeti.integral_finiteMean_sub_sq: the same identity for real random variables.
• TauCeti.integral_norm_finiteMean_sub_sq_of_forall_eq and TauCeti.integral_norm_finiteMean_sub_sq_le_of_forall_le: the mean-square error is γ / r when every per-sample error equals γ, and at most γ / r when every one is at most γ.

References

• R. Vershynin, High-Dimensional Probability (2018), §1.3: the variance of sums of independent random variables.

theorem TauCeti.integral_norm_sum_sq_of_pairwise_integral_inner_eq_zero {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : ι → Ω → E} {s : Finset ι} (hint : ∀ i ∈ s, ∀ j ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (X i ω) (X j ω)) μ) (horth : (↑s).Pairwise fun (i j : ι) => ∫ (ω : Ω), inner ℝ (X i ω) (X j ω) ∂μ = 0) : ∫ (ω : Ω), ‖∑ i ∈ s, X i ω‖ ^ 2 ∂μ = ∑ i ∈ s, ∫ (ω : Ω), ‖X i ω‖ ^ 2 ∂μ

The second moment of a finite sum of pairwise orthogonal random vectors is the sum of their second moments. Only integrability of the pairwise inner products is required.

theorem TauCeti.integral_norm_sum_sq_of_pairwise_indepFun {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → E} {s : Finset ι} (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (hindep : (↑s).Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) μ) : ∫ (ω : Ω), ‖∑ i ∈ s, X i ω‖ ^ 2 ∂μ = ∑ i ∈ s, ∫ (ω : Ω), ‖X i ω‖ ^ 2 ∂μ

Bienaymé's identity for random vectors. If the random vectors X i, i ∈ s, in a real Hilbert space are square-integrable, centered and pairwise independent, then the expected squared norm of their sum is the sum of their expected squared norms.

theorem TauCeti.integral_norm_finiteMean_sub_sq {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [Nonempty ι] [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → E} {m : E} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ (i : ι), ∫ (x : Ω), X i x ∂μ = m) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) μ) : ∫ (ω : Ω), ‖(finiteMean ℝ fun (x : ι) => X x ω) - m‖ ^ 2 ∂μ = (↑(Fintype.card ι) ^ 2)⁻¹ * ∑ i : ι, ∫ (ω : Ω), ‖X i ω - m‖ ^ 2 ∂μ

The mean-square error of a sample mean. If the random vectors X i in a real Hilbert space are square-integrable, pairwise independent and have a common mean m, then their sample mean S satisfies ∫ ‖S - m‖² = r⁻² ∑ᵢ ∫ ‖X i - m‖², where r is the number of samples.

theorem TauCeti.integral_finiteMean_sub_sq {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype ι] [Nonempty ι] [MeasureTheory.IsProbabilityMeasure μ] {Z : ι → Ω → ℝ} {c : ℝ} (hZ : ∀ (i : ι), MeasureTheory.MemLp (Z i) 2 μ) (hmean : ∀ (i : ι), ∫ (x : Ω), Z i x ∂μ = c) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (Z i) (Z j) μ) : ∫ (ω : Ω), ((finiteMean ℝ fun (x : ι) => Z x ω) - c) ^ 2 ∂μ = (↑(Fintype.card ι) ^ 2)⁻¹ * ∑ i : ι, ∫ (ω : Ω), (Z i ω - c) ^ 2 ∂μ

The mean-square error of a sample mean of real random variables. If the real random variables Z i are square-integrable, pairwise independent and have a common mean c, then their sample mean S satisfies ∫ (S - c)² = r⁻² ∑ᵢ ∫ (Z i - c)², where r is the number of samples.

theorem TauCeti.integral_norm_finiteMean_sub_sq_of_forall_eq {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [Nonempty ι] [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → E} {m : E} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ (i : ι), ∫ (x : Ω), X i x ∂μ = m) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) μ) {γ : ℝ} (hγ : ∀ (i : ι), ∫ (ω : Ω), ‖X i ω - m‖ ^ 2 ∂μ = γ) : ∫ (ω : Ω), ‖(finiteMean ℝ fun (x : ι) => X x ω) - m‖ ^ 2 ∂μ = γ / ↑(Fintype.card ι)

If, in addition to the hypotheses of TauCeti.integral_norm_finiteMean_sub_sq, every sample has the same mean-square error γ, then the sample mean has mean-square error γ / r, where r is the number of samples.

theorem TauCeti.integral_norm_finiteMean_sub_sq_le_of_forall_le {Ω : Type u_1} {ι : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [Nonempty ι] [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → E} {m : E} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ (i : ι), ∫ (x : Ω), X i x ∂μ = m) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) μ) {γ : ℝ} (hγ : ∀ (i : ι), ∫ (ω : Ω), ‖X i ω - m‖ ^ 2 ∂μ ≤ γ) : ∫ (ω : Ω), ‖(finiteMean ℝ fun (x : ι) => X x ω) - m‖ ^ 2 ∂μ ≤ γ / ↑(Fintype.card ι)

If, in addition to the hypotheses of TauCeti.integral_norm_finiteMean_sub_sq, every sample has mean-square error at most γ, then the sample mean has mean-square error at most γ / r, where r is the number of samples.