Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.WeakNormInput

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

Weak-norm inputs for the coarse-fluctuation lemma

This file instantiates the deterministic weak-norm maximizer theorem at the special vectors and beta-shifted Section 5.3 exponents.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.ae_specialWeakNormsMaximizer_homogenizationScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k < m) (e : Vec d) : ∀ᵐ (a : RegCoeffField d) ∂P, have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 2 * β; have s' := hP4.sLower + β; have t := hP4.sUpper + 2 * β; have t' := hP4.sUpper + β; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; have p0_e := (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ • q_e - p_e; have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e; Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d ↑m) s p_e q_e p0_e a.toFun ≤ 2 * WeakNormsMaximizer.gradientRHSAtScale (WeakNormsMaximizer.section53WeakNormMaximizerConst d) (↑m) (↑k) s s' p_e q_e p0_e a ∧ Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d ↑m) t p_e q_e q0_e a.toFun ≤ 2 * WeakNormsMaximizer.fluxRHSAtScale (WeakNormsMaximizer.section53WeakNormMaximizerConst d) (↑m) (↑k) t t' p_e q_e q0_e a

Almost-sure beta-shifted weak-norm bounds for the special-vector scalar maximizer. This is the direct bridge from the second Section 5.3 lemma into the third one.