Projection

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

Variance as the smallest quadratic distance to a constant

Two elementary L² facts underlying the opening step in the proof of t.block.variance: Var[F] ≤ 𝔼[(F − 𝔼[F_σ])²] ≤ 2·𝔼[|F − F_σ|²] + 2·Var[F_σ].

• variance_le_integral_sub_const : Var[F] ≤ ∫ (F − c)² for any constant c (variance is the smallest mean-square distance to a constant).
• var_le_two_integral_add_two_var : the (x+y)² ≤ 2x² + 2y² split, taking c = 𝔼[G] so the second term is exactly Var[G].

theorem HCPolySupport.variance_le_integral_sub_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {F : Ω → ℝ} (hF : MeasureTheory.MemLp F 2 μ) (c : ℝ) : ProbabilityTheory.variance F μ ≤ ∫ (ω : Ω), (F ω - c) ^ 2 ∂μ

Variance is the smallest quadratic distance to a constant.

theorem HCPolySupport.var_le_two_integral_add_two_var {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {F G : Ω → ℝ} (hF : MeasureTheory.MemLp F 2 μ) (hG : MeasureTheory.MemLp G 2 μ) : ProbabilityTheory.variance F μ ≤ 2 * ∫ (ω : Ω), (F ω - G ω) ^ 2 ∂μ + 2 * ProbabilityTheory.variance G μ

The (x+y)² ≤ 2x² + 2y² split. With c = 𝔼[G], the constant-distance bound of variance_le_integral_sub_const becomes 2·∫(F−G)² + 2·Var[G].