High-contrast homogenization: Provider.Regularity.ResponseExponentGap

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Changing the summability exponent of the response error

The normalized response error with outer exponent one is controlled by the outer-exponent-two error at any strictly smaller fractional order. The loss is the geometric-series factor associated with the gap between the two orders.

theorem HCPolySupport.HighContrast.homogenizationErrorOnCube_infinity_one_le_gap_mul_infinity_two {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) (a0 : Mat d) {b r : ℝ} (hb : 0 < b) (hbr : b < r) : Book.Ch02.HomogenizationErrorOnCube Q r Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 1) a a0 ≤ Book.Ch02.geometricDiscount r 1 * (√(Book.Ch02.geometricDiscount (r - b) 2))⁻¹ * (√(Book.Ch02.geometricDiscount b 2))⁻¹ * Book.Ch02.HomogenizationErrorOnCube Q b Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a a0

The q = 1 response error at order r is controlled by the q = 2 response error at every smaller positive order b.