High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitDeepened #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The burn-split deepened mean envelope and its collapse #
The clause-2 chain at the burn-split frame: the mean of an enclosed cell
is dominated by the reference at 2·(deepened first moment of the enlarged source), hence by the absolute constant 4 past the
burn-in — no boundary constant, no grid-norm power. The comparability is
restated at an abstract collapsed coefficient, so the burn-split constant
feeds it directly.
theorem
HCPolySupport.HighContrast.Quenched.adaptedMean_le_scaled_burnsplit
{d : ℕ}
(hd : 2 ≤ d)
{g : ℝ}
(hg : g ∈ Set.Ico 0 1)
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{E : BlockMat d}
{Ψ' : ℝ → ℝ}
{K' : ℝ}
{Sh : CoeffSpace d → ℝ}
(hdag' : CoarseEllipticityDagger P g E Ψ' K' Sh)
{G : ℕ}
(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 * ↑(G + 1) - ↑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 ^ (G + 1))
{sKw : ℤ}
(hsKw : growthBar K' ≤ 3 ^ sKw)
(k : ℤ)
(M : ℕ)
(hDk : 0 ≤ k + ↑(G + 1) - 1 - sKw)
(hsub : adaptedCell (roundedGrid l n) k ⊆ centeredCube d (k + ↑(G + 1)))
(hint : HasFiniteAdaptedMean P (roundedGrid l n) k)
:
The burn-split deepened mean envelope. The window height is
G + 1, matching the moment interface.
theorem
HCPolySupport.HighContrast.Quenched.adaptedMean_le_scaled_burnsplit_collapsed
{d : ℕ}
(hd : 2 ≤ d)
{g : ℝ}
(hg : g ∈ Set.Ico 0 1)
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{E : BlockMat d}
{Ψ' : ℝ → ℝ}
{K' : ℝ}
{Sh : CoeffSpace d → ℝ}
(hdag' : CoarseEllipticityDagger P g E Ψ' K' Sh)
{G : ℕ}
(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 * ↑(G + 1) - ↑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 ^ (G + 1))
{sKw : ℤ}
(hsKw : growthBar K' ≤ 3 ^ sKw)
(k : ℤ)
(M : ℕ)
(hDk : 0 ≤ k + ↑(G + 1) - 1 - sKw)
(hburnk :
1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K')) * growthBar K' ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(k + ↑(G + 1) - 1 - sKw)))
(hsub : adaptedCell (roundedGrid l n) k ⊆ centeredCube d (k + ↑(G + 1)))
(hint : HasFiniteAdaptedMean P (roundedGrid l n) k)
:
BlockMatLoewnerLE (adaptedMean P (roundedGrid l n) k) (blockScale 4 E)
The collapsed burn-split mean envelope: past the burn-in the
coefficient is the absolute constant 4.
theorem
HCPolySupport.HighContrast.Quenched.terminal_reference_comparability_of_c1
{d : ℕ}
[NeZero d]
(hd : 2 ≤ d)
{g : ℝ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
{l : ℤ}
(hl : ↑(kZero d) ≤ l)
{n : Mat d}
(hn : Matrix.PosDef n)
(t : ℤ)
(hint : HasFiniteAdaptedMean P (roundedGrid l n) t)
{c1 : ℝ}
(hc11 : 1 ≤ c1)
(hmean : BlockMatLoewnerLE (adaptedMean P (roundedGrid l n) t) (blockScale c1 E))
:
1 ≤ kappaRef E * c1 ∧ ∀ (X : BlockVec d),
blockVecDot X (blockMatVecMul E X) ≤ kappaRef E * c1 * blockVecDot X (blockMatVecMul (adaptedMean P (roundedGrid l n) t) X)
The comparability at an abstract collapsed coefficient.