High-contrast homogenization: Provider.Response.DiagonalWeakNormGood #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_good_le
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(H : ℕ)
{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 ≠ ⊤)
(hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta)
:
(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
(4 * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * (diagonalWeakCellSum q t H s E a + diagonalWeakAverageSum q t H s rho E a) + √2 * diagonalWeakMetricFactor m E * diagonalWeakEnergy hq t a p r * (8 * (√delta)⁻¹ / (2 * s - rho) * 3 ^ (-((s - rho / 2) * ↑(H + 1)))))
The released split level #
theorem
HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_good_at_level_le
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(H : ℕ)
{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)
{a : CoeffSpace d}
(p r : Vec d)
(hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤)
(hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta)
:
(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
(recentConstantAtLevel delta * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * (diagonalWeakCellSum q t H s E a + diagonalWeakAverageSum q t H s rho E a) + √2 * diagonalWeakMetricFactor m E * diagonalWeakEnergy hq t a p r * (4 * (1 + √delta) / (2 * s - rho) * 3 ^ (-((s - rho / 2) * ↑(H + 1)))))
The good branch of the all-scale estimate, at a released split level.