Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.FinalRHS

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

Final RHS conversion for the coarse-fluctuation lemma

This proof-internal file collects the already proved expectation estimates into the manuscript coarse-fluctuation RHS.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.specialWeakNormManuscriptRHSAtScale_le_coarseFluctuationManuscriptRHSAtScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {k m : ℕ}, k < m → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → specialWeakNormManuscriptRHSAtScale hP hStruct hP4 k m e ≤ coarseFluctuationManuscriptRHSAtScale hP hStruct hP4 C ε k m e

The first-lemma special-vector RHS is bounded by the final manuscript coarse-fluctuation RHS.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.JUpperBoundCoarseFluctuations_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {k m : ℕ}, k < m → ∀ (e : Vec d), vecNormSq 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 ≤ coarseFluctuationManuscriptRHSAtScale hP hStruct hP4 C ε k m e

The third Section 5.3 coarse-fluctuation lemma, assembled from the first-lemma special-vector estimate and the final RHS conversion.