Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.HarmonicReplacementNegativeBesovAtErrorOrder

High-contrast homogenization: Provider.Regularity.HarmonicReplacementNegativeBesovAtErrorOrder #

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

Harmonic replacement at a prescribed response-error order #

The two-exponent comparison theorem permits the negative Besov output order to be chosen independently of the response-error order. A positive gap larger than a factor of two is sufficient for the identity-harmonic replacement.

source
theorem HCPolySupport.HighContrast.exists_identityHarmonicReplacementNegativeBesovEstimateConstant_at_error_order (d : ℕ) [NeZero d] (sOut b : ℝ) (hb : 0 < b) (h2b : 2 * b < sOut) (hsOut_lt : sOut < 1) :
∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch03.CoeffFamily d) (m : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier) (hu : IsWeakSolutionOn (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier u.grad), Book.Ch03.homogenizationComparisonNegativeBesovLHS (originCube d m) a (identityConstantCoeffMatrix d) sOut (identityHarmonicReplacementDatum a m u hu).u (identityHarmonicReplacementDatum a m u hu).v ≤ C * scalarIdentityWeakError a b m * Book.Ch03.h1EnergyNormOnCube (originCube d m) a u

At every output order strictly larger than twice the response-error order, the chosen identity-harmonic replacement is controlled by that response error.