High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.HomogenizationErrorAllDepthMajorant
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
All-depth majorants for the cube homogenization error #
The squared p = infinity, q = 2 homogenization error is the weighted sum
of the descendant response maxima. Consequently, any summable pointwise
majorant for that row gives a majorant for the complete error.
theorem
HCPolySupport.HighContrast.RowSupply.homogenizationErrorOnCube_infinity_two_sq_le_tsum_of_max_le
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(a : Book.Ch02.TriadicCoeffFamily d)
(a0 : Mat d)
(B : ℕ → ℝ)
(hB : Summable fun (l : ℕ) => Book.Ch02.geometricWeight s 2 l * B l)
(hmax : ∀ (l : ℕ), Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑l) a a0 ≤ B l)
:
Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a
a0 ^ 2 ≤ ∑' (l : ℕ), Book.Ch02.geometricWeight s 2 l * B l
A summable pointwise majorant for every descendant response row controls the complete squared homogenization error.
theorem
HCPolySupport.HighContrast.RowSupply.homogenizationErrorOnCube_infinity_two_le_sqrt_tsum_of_max_le
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(a : Book.Ch02.TriadicCoeffFamily d)
(a0 : Mat d)
(B : ℕ → ℝ)
(hB : Summable fun (l : ℕ) => Book.Ch02.geometricWeight s 2 l * B l)
(hmax : ∀ (l : ℕ), Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑l) a a0 ≤ B l)
:
Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a
a0 ≤ √(∑' (l : ℕ), Book.Ch02.geometricWeight s 2 l * B l)
The corresponding unsquared estimate, in the form consumed by response pricing, is obtained by taking the nonnegative square root.