Coarse-graining support: Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms

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

Upper bound for J by weak norms

Top-level module for the first manuscript lemma in Section 5.3. The proof is split under Section53/JUpperBoundWeakNorms/; this file is the stable import surface for the lemma.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms_homogenizationScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) {s t : ℝ} (hs : 0 < s) (hs_lt_one : s < 1) (ht : 0 < t) (hst : s + t ≤ 1) (p q p0 q0 : Vec d) (hGradSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d m) s p q p0 a.toFun ^ 2) P) (hFluxSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d m) t p q q0 a.toFun ^ 2) P) : have Q := originCube d m; have j := (m - k).toNat; Ch04.expectedResponseJCubeSet P Q p q - 1 / 2 * vecDot p0 q0 ≤ JUpperBoundWeakNorms.jUpperWeakNormManuscriptExpectedRHSAtScale P m k s t (1 + JUpperBoundWeakNorms.section53CutoffBound Q) (JUpperBoundWeakNorms.section53CutoffOscillationConstant Q) (JUpperBoundWeakNorms.section53CutoffScaleSep Q j) (JUpperBoundWeakNorms.section53CutoffDualBound Q s) (JUpperBoundWeakNorms.section53CutoffDualBound Q t) (JUpperBoundWeakNorms.section53CutoffProductCoeff Q s t) p q p0 q0

First manuscript lemma of Section 5.3, in its note-facing form up to the finite-RHS inputs supplied by the scalar maximizer weak-norm lemma. The two integrability hypotheses say exactly that the scaled gradient and flux weak-norm square expectations appearing on the right-hand side are finite.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms_young_homogenizationScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) {s t : ℝ} (hs : 0 < s) (hs_lt_one : s < 1) (ht : 0 < t) (hst : s + t ≤ 1) (p q p0 q0 : Vec d) {η : ℝ} (hη : 0 < η) (hGradSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d m) s p q p0 a.toFun ^ 2) P) (hFluxSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d m) t p q q0 a.toFun ^ 2) P) : have Q := originCube d m; have j := (m - k).toNat; Ch04.expectedResponseJCubeSet P Q p q - 1 / 2 * vecDot p0 q0 ≤ JUpperBoundWeakNorms.jUpperWeakNormYoungManuscriptExpectedRHSAtScale P m k s t (1 + JUpperBoundWeakNorms.section53CutoffBound Q) (JUpperBoundWeakNorms.section53CutoffOscillationConstant Q) (JUpperBoundWeakNorms.section53CutoffScaleSep Q j) (JUpperBoundWeakNorms.section53CutoffDualBound Q s) (JUpperBoundWeakNorms.section53CutoffDualBound Q t) (JUpperBoundWeakNorms.section53CutoffProductCoeff Q s t) η p q p0 q0

First Section 5.3 lemma with the additivity term treated by Young rather than by Cauchy in probability. This is the surface used by the flatness-rules route: the RHS contains eta * E[J_k] + eta^{-1} * tau_{m,k} instead of sqrt(tau_{m,k}) * sqrt(E[J_k]).