High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedResponseQuenchedRow #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Normalized cube response from a quenched block row #
The exact identity-normalized response on a reference origin cube is bounded
by the physical quenched row on a centered enlargement. The response depth
weight and the boundary-filling loss leave the positive exponent gap
2 * s - rho.
theorem
HCPolySupport.HighContrast.homogenizationErrorOnCube_normalizedReference_infinity_two_sq_le_row
{d : ℕ}
[NeZero d]
(t G : ℕ)
(a : CoeffSpace d)
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
(aRef : Book.Ch03.CoeffFamily d)
(haRef :
∀ (Q : TriadicCube d),
(aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯
((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ ↑t)).toCoeffField)
(s rho sourceScale : ℝ)
(hrho : 0 < rho)
(hrho1 : rho ≤ 1)
(hrhoGap : rho < 2 * s)
(henclose : adaptedCell (Selection.normalizedRoot (symmPart abar)) ↑t ⊆ centeredCube d ↑(t + G))
(hactive : sourceScale ≤ 3 ^ (t + G))
:
Book.Ch02.HomogenizationErrorOnCube (originCube d ↑t) s Book.Ch02.MultiscaleExponent.infinity
(Book.Ch02.MultiscaleExponent.finite 2) aRef 1 ^ 2 ≤ max 1 (6 * ↑d * √↑d * ‖(Selection.normalizedRoot (symmPart abar))⁻¹‖) * 3 ^ (rho * ↑G) * (1 / (1 - 3 ^ (-(2 * s - rho)))) * Quenched.quenchedBlockRow rho (Book.Ch02.constantBlockMatrix abar) sourceScale a (t + G)
The q = 2 normalized reference-cube error is controlled by the physical
quenched block row on a centered enlargement.