The Efron–Stein inequality

This file proves the Efron–Stein inequality for a square-integrable measurable function of independent coordinates, stated on Measure.pi over an arbitrary finite index type. If X has law Measure.pi μ, then Var f(X) ≤ ∑ i, E[Var_i f(X)], where Var_i f(x) is the variance of y ↦ f (Function.update x i y) under μ i, i.e. the variance of f in the i-th coordinate with all other coordinates frozen.

The two-factor law of total variance evariance_prod_eq and Jensen bound evariance_integral_prod_le yield the two-factor Efron–Stein inequality evariance_prod_le. The finite-coordinate proof is by induction on the number of coordinates, followed by transport along an equivalence Fin n ≃ ι.

Main results

• TauCeti.Probability.efronStein: the Efron–Stein inequality on Measure.pi over a finite index type, with arbitrary (dependent) coordinate spaces.

References

• B. Efron and C. Stein, The jackknife estimate of variance, Ann. Statist. 9 (1981), 586–596.
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities, Oxford University Press (2013), Theorem 3.1.

theorem TauCeti.Probability.efronStein {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {f : ((i : ι) → α i) → ℝ} (hf : Measurable f) (hL : MeasureTheory.MemLp f 2 (MeasureTheory.Measure.pi μ)) : ProbabilityTheory.evariance f (MeasureTheory.Measure.pi μ) ≤ ∑ i : ι, ∫⁻ (x : (i : ι) → α i), ProbabilityTheory.evariance (fun (y : α i) => f (Function.update x i y)) (μ i) ∂MeasureTheory.Measure.pi μ

The Efron–Stein inequality on Measure.pi over a finite index type: for a square integrable measurable function f of independent coordinates, the variance of f is at most the sum over i of the average variance of f in coordinate i with the other coordinates frozen.