Coarse-graining support: Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ScalarL2

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Scalar L2 reduction for good-scale probes

This file contains the probabilistic real-variable step used after the subadditivity positive-part estimate: if the positive excess over the annealed base is controlled by a small deterministic error plus a centered partition average, then the full square fluctuation is controlled by the L1 and L2 sizes of that partition average.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_abs_sub_sq_le_of_positivePart_control {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X Z : Ω → ℝ} {base err : ℝ} (hbase_nonneg : 0 ≤ base) (_herr_nonneg : 0 ≤ err) (hX_nonneg : ∀ᵐ (ω : Ω) ∂μ, 0 ≤ X ω) (hmean_lower : base ≤ ∫ (ω : Ω), X ω ∂μ) (hX_int : MeasureTheory.Integrable X μ) (hpos_int : MeasureTheory.Integrable (fun (ω : Ω) => max (X ω - base) 0 ^ 2) μ) (hneg_int : MeasureTheory.Integrable (fun (ω : Ω) => max (base - X ω) 0 ^ 2) μ) (hpos_one_int : MeasureTheory.Integrable (fun (ω : Ω) => max (X ω - base) 0) μ) (hneg_one_int : MeasureTheory.Integrable (fun (ω : Ω) => max (base - X ω) 0) μ) (hZ_abs_int : MeasureTheory.Integrable (fun (ω : Ω) => |Z ω|) μ) (hZ_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => |Z ω| ^ 2) μ) (hpos : (fun (ω : Ω) => max (X ω - base) 0) ≤ᵐ[μ] fun (ω : Ω) => err + |Z ω|) : ∫ (ω : Ω), |X ω - base| ^ 2 ∂μ ≤ 4 * err ^ 2 + 4 * ∫ (ω : Ω), |Z ω| ^ 2 ∂μ + 2 * base * (err + ∫ (ω : Ω), |Z ω| ∂μ)

Real/probability L2 reduction for one scalar probe.

The assumptions are intentionally proof-facing and will be supplied internally for the coordinate and pair probes; the public Section 5.4 theorem does not expose these measurability or integrability packages.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_abs_sub_sq_le_of_positivePart_control_of_centered_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X Z : Ω → ℝ} {base err : ℝ} (hbase_nonneg : 0 ≤ base) (herr_nonneg : 0 ≤ err) (hX_nonneg : ∀ᵐ (ω : Ω) ∂μ, 0 ≤ X ω) (hmean_lower : base ≤ ∫ (ω : Ω), X ω ∂μ) (hX_int : MeasureTheory.Integrable X μ) (hcenter_abs_int : MeasureTheory.Integrable (fun (ω : Ω) => |X ω - base|) μ) (hcenter_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => |X ω - base| ^ 2) μ) (hZ_abs_int : MeasureTheory.Integrable (fun (ω : Ω) => |Z ω|) μ) (hZ_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => |Z ω| ^ 2) μ) (hpos : (fun (ω : Ω) => max (X ω - base) 0) ≤ᵐ[μ] fun (ω : Ω) => err + |Z ω|) : ∫ (ω : Ω), |X ω - base| ^ 2 ∂μ ≤ 4 * err ^ 2 + 4 * ∫ (ω : Ω), |Z ω| ^ 2 ∂μ + 2 * base * (err + ∫ (ω : Ω), |Z ω| ∂μ)

A caller-friendly version of integral_abs_sub_sq_le_of_positivePart_control, deriving the positive and negative part integrability facts from centered L1/L2 integrability.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_abs_and_sq_le_of_annealedMomentRoot_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ξ : ℕ} {Z : Ω → ℝ} {K : ℝ} (hξ : 2 ≤ ξ) (hZ_aemeas : AEMeasurable Z μ) (hZξ_int : MeasureTheory.Integrable (fun (ω : Ω) => |Z ω| ^ ξ) μ) (hroot : (∫ (ω : Ω), |Z ω| ^ ξ ∂μ) ^ (1 / ↑ξ) ≤ K) : ∫ (ω : Ω), |Z ω| ∂μ ≤ K ∧ ∫ (ω : Ω), |Z ω| ^ 2 ∂μ ≤ K ^ 2

Convert the Rosenthal L^ξ root estimate, with ξ ≥ 2, into the L1 and L2 estimates used by integral_abs_sub_sq_le_of_positivePart_control.