High-contrast homogenization: Provider.Response.DiagonalWeakNormOld #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The old-scale tail of the diagonal weak estimate #
On the good branch, the normalized scale-energy estimate is summed only after the recent window. The resulting extended-real tail carries the decay at the edge of that window.
theorem
HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_good_tail_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 ≠ ⊤)
(hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta)
(n : ℕ)
:
∑' (j : ℕ), ENNReal.ofReal
(3 ^ (-(s * ↑(j + n))) * blockAvsumL2 (alignedIndex q (t - ↑(j + n)) t) fun (z : Fin d → ℤ) =>
blockCellAverage (adaptedCellAt q (t - ↑(j + n)) z) 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) * 3 ^ (-((s - rho / 2) * ↑n))))
The normalized weak-seminorm tail after n recent scales obeys the
good-branch geometric bound.
The released split level #
theorem
HCPolySupport.HighContrast.Response.normalized_adaptedWeakSeminorm_good_tail_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)
{a : CoeffSpace d}
(p r : Vec d)
(hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤)
(hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta)
(n : ℕ)
:
∑' (j : ℕ), ENNReal.ofReal
(3 ^ (-(s * ↑(j + n))) * blockAvsumL2 (alignedIndex q (t - ↑(j + n)) t) fun (z : Fin d → ℤ) =>
blockCellAverage (adaptedCellAt q (t - ↑(j + n)) z) 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) / (2 * s - rho) * 3 ^ (-((s - rho / 2) * ↑n))))
The good old-scale tail of the all-scale estimate, at a released split level.