High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitSuccessorEnvelope

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

The burn-split maximal envelope over the window's successor scale

The mesoscale envelope the burn split consumes — the truncated standard-cube bound 3^{g(m-h-k)_+} whose localizing cube sits h scales above the envelope's own base — is the window's own improved discount: badScaleEvent is its negation at depth h, successorScale is the strict successor of the bad scales, and improved_discount_of_successorScale_le is the implication. A coupled window of height h = 2D therefore supplies the input of henvMax_burnsplit_of_isotropyReference outright, and the maximal envelope at the isotropy block holds with the dimension-only constant 4/(1+cIso) over the successor scale of that window.

theorem HCPolySupport.HighContrast.Quenched.mesoEnvelope_of_successorScale {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) {D : ℕ} (hdepth : M - jStar = ↑(2 * D)) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), (successorScale g E (M - jStar) a).toReal ≤ 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)

The mesoscale envelope from the window's successor scale. Almost surely, once the successor scale of a window of height 2D has burned at scale m, every standard cube centered in □_m obeys the truncated envelope 3^{g(m-2D-k)_+}·E.

theorem HCPolySupport.HighContrast.Quenched.henvMax_burnsplit_of_successorScale {d : ℕ} [NeZero d] (hd : 2 ≤ d) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) {D : ℕ} (hdepth : M - jStar = ↑(2 * D)) {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 * (successorScale g E (M - jStar) a).toReal * 3 ^ (-(↑t + ↑D))) ^ g / 2))

The maximal envelope at the isotropy block over the window's successor scale. The burn-split chain with its mesoscale input discharged: the normalizing constant is 4/(1+cIso), with no reference ratio and no boundary constant.