LocalCoarseGraining

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Local finite-p coarse-graining assembly

This is the source-facing assembly point for the frozen local finite-p coarse-graining theorem. The reusable input modules deliberately keep the negative-series expansion, descendant restriction, response localization, and forcing summation separate; this file only combines those literal carriers.

theorem HCPolySupport.Book.Ch03.ABK26.exists_localCoarseGrainingLp (d : ℕ) (hd : 2 ≤ d) : ∃ C < ⊤, ∀ (p : FiniteLpExponent), 2 ≤ p.exponent → ∀ (m n : ℤ) (hnm : n < m) (s1 s s2 : ↑FractionalOrder), ↑s1 < ↑s → ↑s < ↑s2 → ∀ (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (g : Vec d → Vec d), MemCubeEuclideanFullWsp (originCube d m) s2 p g → ∀ (u : H1Function (openCubeSet (originCube d m))), IsForcedEquation (originCube d m) a u g → localFluxDefectNegativeBesovLpAverage (originCube d m) n ⋯ a sigma0 u s p ≤ localCoarseGrainingLpRHS C (originCube d m) n ⋯ a sigma0 hsigma0 g u s1 s s2 p

The exact local finite-p coarse-graining theorem frozen in the Chapter 3 declaration anchors. All regularity, trace, response, and summability work is discharged internally through the one-cube and forcing seams.