High-contrast homogenization: Provider.Response.DiagonalWeakNormBad #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The all-scale bad branch of the diagonal weak estimate #
When the response maximum exceeds the threshold, the single-scale energy bound is summable over every scale. The extended-real seminorm is therefore controlled by the bad-event geometric majorant.
theorem
HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_bad_le
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
{S m : Mat d}
(hsymm : matTranspose S = S)
(hsq : S * S = m)
(hm : Matrix.PosDef m)
{E : BlockMat d}
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
{rho s delta : ℝ}
(hrho : 0 < rho)
(hs : rho / 2 < s)
(hs1 : s ≤ 1)
(hdelta : 0 < delta)
(hdelta1 : delta ≤ 1)
{a : CoeffSpace d}
(p r : Vec d)
(hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤)
(hbad : delta < (diagonalWeakMaximum rho q t E a).toReal)
:
(ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s fun (x : Vec d) =>
blockMatVecMul (Book.Ch02.blockDiag S S⁻¹)
(diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ ENNReal.ofReal
(√2 * diagonalWeakMetricFactor m E * diagonalWeakEnergy hq t a p r * (8 * (√delta)⁻¹ / (2 * s - rho) * √(diagonalWeakMaximum rho q t E a).toReal))
On the branch where the response maximum exceeds delta, the normalized
weak seminorm of the centered canonical state has the all-scale bound.
The released split level #
theorem
HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_bad_at_level_le
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
{S m : Mat d}
(hsymm : matTranspose S = S)
(hsq : S * S = m)
(hm : Matrix.PosDef m)
{E : BlockMat d}
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
{rho s delta : ℝ}
(hrho : 0 < rho)
(hs : rho / 2 < s)
(hs1 : s ≤ 1)
(hdelta : 0 < delta)
{a : CoeffSpace d}
(p r : Vec d)
(hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤)
(hbad : delta < (diagonalWeakMaximum rho q t E a).toReal)
:
(ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s fun (x : Vec d) =>
blockMatVecMul (Book.Ch02.blockDiag S S⁻¹)
(diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ ENNReal.ofReal
(√2 * diagonalWeakMetricFactor m E * diagonalWeakEnergy hq t a p r * (4 * (1 + √delta) * (√delta)⁻¹ / (2 * s - rho) * √(diagonalWeakMaximum rho q t E a).toReal))
The bad branch of the all-scale estimate, at a released split level.