Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ProbeMomentCompression

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

Compressed origin moments for variance probes

The first Rosenthal bridge used the coarse bound C * (Λ + λ⁻¹). For the final variance lemma we also need the sharper matched form CUpper * Λ + CLower * λ⁻¹, so that good-scale scalar comparisons compress the normalization constants to \widetilde\Theta_0.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54_centeredOrigin_momentRoot_le_weighted_factor_sum_of_abs_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {CUpper CLower : ℝ} (hCUpper_nonneg : 0 ≤ CUpper) (hCLower_nonneg : 0 ≤ CLower) {X : RegCoeffField d → ℝ} (hX_meas : AEMeasurable X P) (hX_abs_le : (fun (a : RegCoeffField d) => |X a|) ≤ᵐ[P] fun (a : RegCoeffField d) => CUpper * Ch04.LambdaSqCoeffField (originCube d 0) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a + CLower * (Ch04.lambdaSqCoeffField (originCube d 0) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a - ∫ (b : RegCoeffField d), X b ∂P| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |X a - ∫ (b : RegCoeffField d), X b ∂P|) ≤ 2 * (CUpper * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + CLower * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)

Centered origin moment bound from a matched upper/lower unit-scale ellipticity domination.