High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentHead #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Response.normalized_diagonalWeak_recent_head_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)
(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)
:
∑ j ∈ Finset.range (H + 1),
ENNReal.ofReal
(3 ^ (-(s * ↑j)) * blockAvsumL2 (alignedIndex q (t - ↑j) t) fun (w : Fin d → ℤ) =>
blockCellAverage (adaptedCellAt q (t - ↑j) w) 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))
The released split level #
theorem
HCPolySupport.HighContrast.Response.normalized_diagonalWeak_recent_head_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)
{a : CoeffSpace d}
(p r : Vec d)
(hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤)
(hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta)
:
∑ j ∈ Finset.range (H + 1),
ENNReal.ofReal
(3 ^ (-(s * ↑j)) * blockAvsumL2 (alignedIndex q (t - ↑j) t) fun (w : Fin d → ℤ) =>
blockCellAverage (adaptedCellAt q (t - ↑j) w) 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))
The recent head block of the all-scale estimate, at a released split level.