Coarse-graining support: Support.Book.Ch05.Theorems.Section53.WeakNormsMaximizer.AssemblyFinal

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

Final assembly for the weak-norm maximizer lemma

This file finishes the deterministic weak-norm maximizer theorem from the scale-geometric core estimates.

theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.weakNormsMaximizerGradient_homogenizationScale {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) {k m : ℤ} (hkm : k < m) {s s' : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hs'_low : s / 2 ≤ s') (hs'_high : s' < s) (p q p0 : Vec d) : Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d m) s p q p0 a.toFun ≤ 2 * gradientRHSAtScale (section53WeakNormMaximizerConst d) m k s s' p q p0 a

Deterministic gradient weak-norm bound for the scalar response maximizer at homogenization scale. The leading factor 2 records the current high/low split normalization and is absorbed harmlessly in later constants.

theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.weakNormsMaximizerFlux_homogenizationScale {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) {k m : ℤ} (hkm : k < m) {t t' : ℝ} (ht : 0 < t) (ht_le : t ≤ 1) (ht'_low : t / 2 ≤ t') (ht'_high : t' < t) (p q q0 : Vec d) : Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d m) t p q q0 a.toFun ≤ 2 * fluxRHSAtScale (section53WeakNormMaximizerConst d) m k t t' p q q0 a

Deterministic flux weak-norm bound for the scalar response maximizer at homogenization scale. The leading factor 2 records the accepted split loss and is absorbed harmlessly in later constants.

theorem HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.weakNormsMaximizer_homogenizationScale {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) {k m : ℤ} (hkm : k < m) {s s' t t' : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hs'_low : s / 2 ≤ s') (hs'_high : s' < s) (ht : 0 < t) (ht_le : t ≤ 1) (ht'_low : t / 2 ≤ t') (ht'_high : t' < t) (p q p0 q0 : Vec d) : Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d m) s p q p0 a.toFun ≤ 2 * gradientRHSAtScale (section53WeakNormMaximizerConst d) m k s s' p q p0 a ∧ Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d m) t p q q0 a.toFun ≤ 2 * fluxRHSAtScale (section53WeakNormMaximizerConst d) m k t t' p q q0 a

The paired deterministic weak-norm maximizer estimate, in the manuscript parameter regime.