Coarse-graining support: Support.Book.Ch03.Theorems.GeneralCoarseGrainingL2TwoExponent

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

Scale-separated general coarse-graining handoff

This file contains the repaired inhomogeneous Ch3.3 general coarse-graining surface. The local flux-response exponent and the positive forcing exponent are separated, so the forcing term carries the visible inverse depth factor 3^{-r₂(m-n)}.

structure HCPolySupport.Book.Ch03.GeneralCoarseGrainingL2TwoExponentTheory (d : ℕ) [NeZero d] : Prop

Public general coarse-graining package with a stronger force exponent.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {a0 : ConstantCoeffMatrix d} {s r r₂ : ℝ} {j : ℕ} {g : Vec d → Vec d}, IsPositiveScalarMatrix a0.matrix → ∀ (w : CoarseGrainingComparisonDatum Q a a0 g), 0 < s → 0 < r → r < s / 2 → s < 1 → r ≤ r₂ → ForceBesovRegularity Q r₂ g → homogenizationComparisonNegativeBesovLHS Q a a0 s w.u w.v ≤ generalCoarseGrainingL2TwoExponentRHS C Q a a0 s r r₂ j g w.u

theorem HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentTheory (d : ℕ) [NeZero d] : GeneralCoarseGrainingL2TwoExponentTheory d

Public Ch3.3 scale-separated general coarse-graining package with all currently formalized analytic inputs discharged.