High-contrast homogenization: Provider.Response.DiagonalWeakNormAdjoint #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The adjoint diagonal weak estimate #
The primal estimate for the transposed coefficient is applied with the signed congruence of the reference block. All source carriers are then read back at the original coefficient and reference.
theorem
HCPolySupport.HighContrast.Response.diagonalWeakNorm_adjoint_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)
(hrho2 : rho < 2)
(hs : rho / 2 < s)
(hs1 : s ≤ 1)
(hdelta : 0 < delta)
(hdelta1 : delta ≤ 1)
(a : CoeffSpace d)
(p r : Vec d)
:
(ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s fun (x : Vec d) =>
blockMatVecMul (Book.Ch02.blockDiag S S⁻¹)
(diagonalWeakAdjointState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t a p r))) ≤ if diagonalWeakMaximum rho q t E a = ⊤ then ⊤
else ENNReal.ofReal
(16 * diagonalWeakMetricFactor m E * diagonalWeakLoadPlus E p r * (diagonalWeakCellSum q t H s E a + diagonalWeakAverageSum q t H s rho E a) + (16 * (√delta)⁻¹ / (2 * s - rho) * diagonalWeakMetricFactor m E * if delta < (diagonalWeakMaximum rho q t E a).toReal then √(diagonalWeakMaximum rho q t E a).toReal
else 3 ^ (-((s - rho / 2) * ↑H))) * diagonalWeakAdjointEnergy hq t a p r)
The released split level #
theorem
HCPolySupport.HighContrast.Response.diagonalWeakNorm_adjoint_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)
(hdelta : 0 < delta)
(a : CoeffSpace d)
(p r : Vec d)
:
(ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm q t s fun (x : Vec d) =>
blockMatVecMul (Book.Ch02.blockDiag S S⁻¹)
(diagonalWeakAdjointState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t a p r))) ≤ if diagonalWeakMaximum rho q t E a = ⊤ then ⊤
else ENNReal.ofReal
(recentConstantAtLevel delta * diagonalWeakMetricFactor m E * diagonalWeakLoadPlus E p r * (diagonalWeakCellSum q t H s E a + diagonalWeakAverageSum q t H s rho E a) + (maxGroupConstantAtLevel delta / (2 * s - rho) * diagonalWeakMetricFactor m E * if delta < (diagonalWeakMaximum rho q t E a).toReal then √(diagonalWeakMaximum rho q t E a).toReal
else 3 ^ (-((s - rho / 2) * ↑H))) * diagonalWeakAdjointEnergy hq t a p r)
The adjoint all-scale estimate at a released split level.