High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitMaximumEnvelope

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The maximal envelope at a dimension-only constant

The parametrized diagonal-weak maximum bound reads the source envelope on adapted cells through the fixed-level Whitney bridge, so its normalizing constant carries the boundary constant C_d 𝔢 ζ_g of the cell conversion and the enlargement factor 3^{gG} of the containment. The printed conversion (Lemma 2.13 of HC, whose conclusion is (2.124)) carries neither: it splits the Whitney rows at a burn depth and absorbs the geometry into a scale restriction, as HC (2.123) records.

The input the printed conversion uses is not the all-scale bound of e.coarse.ellipticity but its mesoscale improvement (Lemma 2.8 of HC, conclusion (2.91)): at burn depth h the standard-cube envelope is the truncated 3^{g(m-h-k)_+}, whose localizing cube □_m sits h scales above the envelope's own base. That gap is what buys the flat band, and this module is the chain over it.

At depth 2D the adapted-cell envelope becomes (1 + C_d 𝔢 ζ_g 3^{-D}) times the truncated 3^{g(m-D-k)_+}, and once the depth absorbs the geometry — boundaryConst ≤ 3^D, the Lean form of HC (2.123) — the ρ-weighted maximal function of the aligned cells obeys the printed envelope (max 1 (3·𝒮·3^{-(t+D)}))^g with the normalizing constant 4/γ: dimensional, with the aspect ratio riding only in the enlargement D and hence in a scale threshold.

theorem HCPolySupport.HighContrast.Quenched.coarseBlock_adaptedCell_burnsplit_le_of_mesoEnvelope {d : ℕ} (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} (hE : Book.Ch02.BlockPosDef E) {Sh : CoeffSpace d → ℝ} {D : ℕ} (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), Sh a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑D - ↑k) 0)) E)) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), Sh a ≤ 3 ^ m → ∀ (k : ℤ) (w : Fin d → ℤ), adaptedCellAt (roundedGrid l n) k w ⊆ centeredCube d m → BlockMatLoewnerLE (coarseBlock (adaptedCellAt (roundedGrid l n) k w) a) (blockScale ((1 + Cd * witnessEccentricity n * zetaG g * 3 ^ (-↑D)) * 3 ^ (g * max (↑m - ↑D - ↑k) 0)) E)

The adapted-cell envelope at the burn split. The mesoscale envelope at depth 2D gives every aligned adapted cell of the fixed grid contained in the cube of scale m the coarse-block bound (1 + C_d 𝔢 ζ_g 3^{-D})·3^{g(m-D-k)_+}·E, with the geometry on 3^{-D} instead of multiplying.

theorem HCPolySupport.HighContrast.Quenched.diagonalWeakMaximum_burnsplit_parametrized_le {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} (hE : Book.Ch02.BlockPosDef E) {Sh : CoeffSpace d → ℝ} {D : ℕ} (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), Sh a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑D - ↑k) 0)) E)) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) (hD : boundaryConst Cd g n ≤ 3 ^ D) {rho : ℝ} (hrho : g ≤ rho) (t : ℤ) (hgeom : ∀ k ≤ t, ∀ w ∈ Response.alignedIndex (roundedGrid l n) k t, adaptedCellAt (roundedGrid l n) k w ⊆ centeredCube d (t + ↑D)) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {gam : ℝ} (hgam : 0 < gam) (hFE : BlockMatLoewnerLE (blockScale gam E) F) : ∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid l n) t F a ≤ ENNReal.ofReal (4 / gam * (max 1 (3 * Sh a * 3 ^ (-(↑t + ↑D))) ^ g / 2))

The weak maximum at a dimension-only normalizer. With the burn depth absorbing the geometry (boundaryConst Cd g n ≤ 3^D, the Lean form of HC (2.123)), the ρ-weighted maximal function of the aligned cells obeys the printed envelope with normalizing constant 4/γ.

theorem HCPolySupport.HighContrast.Quenched.henvMax_burnsplit_of_isotropyReference {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} (hEsym : IsSymmetricBlockMat E) (hE : Book.Ch02.BlockPosDef E) {Sh : CoeffSpace d → ℝ} {D : ℕ} (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), Sh a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑D - ↑k) 0)) E)) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {nu : Mat d} (hnu : Matrix.PosDef nu) (hD : boundaryConst Cd g nu ≤ 3 ^ D) {rho : ℝ} (hrho : g ≤ rho) (t : ℤ) (hgeom : ∀ k ≤ t, ∀ w ∈ Response.alignedIndex (roundedGrid l nu) k t, adaptedCellAt (roundedGrid l nu) k w ⊆ centeredCube d (t + ↑D)) {cIso : ℝ} (hcIso : 0 ≤ cIso) : ∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid l nu) t (isotropyReference cIso E) a ≤ ENNReal.ofReal (4 / (1 + cIso) * (max 1 (3 * Sh a * 3 ^ (-(↑t + ↑D))) ^ g / 2))

The maximal envelope at the isotropy block, with no reference ratio. The burn-split chain read at isotropyReference cIso 𝐄: the normalizing constant is 4/(1+cIso), and neither the boundary constant nor the enlargement factor appears.