Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.OneStepContraction.CoarseFluctuationInput

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

Section 5.3 input for the one-step contraction

This file is the narrow bridge from the public Section 5.3 coarse-fluctuation lemma to the k = 0 special-vector estimate used in the Section 5.4 one-step contraction proof.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.exists_expectedCenteredResponseJAtScale_special_le_coarseFluctuationRHS_zero_uniform {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {m : ℕ}, 0 < m → ∀ (e : Vec d), Ch02.vecNorm e = 1 → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; expectedCenteredResponseJAtScale hP hStruct (↑m) p_e q_e ≤ Section53.JUpperBoundCoarseFluctuations.coarseFluctuationManuscriptRHSAtScale hP hStruct hP4 C ε 0 m e

The public Section 5.3 coarse-fluctuation lemma, specialized to k = 0 and to the Section 5.4 unit-vector convention, with the constant chosen from the fixed (P4) parameters before the law is introduced.