TwoPoint

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Two-point variance identity and a Jensen bound

Building blocks for the Efron–Stein inequality.

• Homogenization.variance_eq_half_integral_sub_sq: for a bounded measurable real random variable X on a probability space, Var[X] = ½ ∫∫ (X a − X b)² dμ dμ.
• Homogenization.sq_integral_le_integral_sq: Jensen's inequality in the form (∫ X)² ≤ ∫ X² for a bounded measurable X on a probability space.

Everything is stated for bounded observables, which makes all integrability side conditions immediate; no L²-generality is attempted.

theorem HCPolySupport.memLp_two_of_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : Measurable X) {M : ℝ} (hM : ∀ (ω : Ω), |X ω| ≤ M) : MeasureTheory.MemLp X 2 μ

A bounded measurable function is MemLp 2 on a probability (finite) measure.

theorem HCPolySupport.integrable_of_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : Measurable X) {M : ℝ} (hM : ∀ (ω : Ω), |X ω| ≤ M) : MeasureTheory.Integrable X μ

A bounded measurable function is integrable on a probability (finite) measure.

theorem HCPolySupport.integrable_sq_of_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : Measurable X) {M : ℝ} (hM : ∀ (ω : Ω), |X ω| ≤ M) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ

The square of a bounded measurable function is integrable.

theorem HCPolySupport.variance_eq_half_integral_sub_sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : Measurable X) {M : ℝ} (hM : ∀ (ω : Ω), |X ω| ≤ M) : ProbabilityTheory.variance X μ = 1 / 2 * ∫ (a : Ω), ∫ (b : Ω), (X a - X b) ^ 2 ∂μ ∂μ

Two-point variance identity. For a bounded measurable real random variable X on a probability space, the variance equals one half of the mean squared difference of two independent samples.

theorem HCPolySupport.sq_integral_le_integral_sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : Measurable X) {M : ℝ} (hM : ∀ (ω : Ω), |X ω| ≤ M) : (∫ (ω : Ω), X ω ∂μ) ^ 2 ≤ ∫ (ω : Ω), X ω ^ 2 ∂μ

Jensen's inequality, (∫ X)² ≤ ∫ X², for a bounded measurable function on a probability space.