High-contrast homogenization: Provider.Quenched.SmallContrastMaximumEnvelope

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

The reference-normalized maximal function under the source envelope

The scale-adapted source envelope bounds every aligned adapted cell by boundaryConst · 3^{g(m−k)} · E on the event that the source has burned at scale m. Measured against the inflated reference boundaryConst·3^{gG}·E covering the generation's geometry, the ρ-weighted all-scale maximal function is therefore at most 1 once the source has burned at the generation's own scale, and at most (3·S·3^{-(t+G)})^g in general — the printed 𝓜_{n,γ} ≤ (3^{-n}𝒮)^γ-type envelope, with no window multiplier.

theorem HCPolySupport.HighContrast.Quenched.coarseBlock_adaptedCell_scaled_le_of_source_burned {d : ℕ} (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {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 : ℤ), S 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 (boundaryConst Cd g n * 3 ^ (g * (↑m - ↑k))) E)

The scale-adapted source envelope for adapted cells: almost surely, at every burn scale m, every adapted cell of the fixed grid contained in the cube of scale m has coarse block at most boundaryConst · 3^{g(m−k)} · E.