High-contrast homogenization: Provider.Regularity.HarmonicReplacementL2AtErrorOrder

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

Identity-harmonic approximation at a prescribed error order

For every positive response-error order below one half, a weak solution on a centered cube admits an identity-harmonic same-trace replacement whose normalized L² error is controlled at that same response-error order.

theorem HCPolySupport.HighContrast.exists_identityHarmonicReplacementL2EstimateConstant_at_error_order (d : ℕ) [NeZero d] (b : ℝ) (hb : 0 < b) (hb_lt : b < 1 / 2) : ∃ (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), (cubeBesovScaleWeight 1 (originCube d m) * cubeLpNorm (originCube d m) 2 fun (x : Vec d) => u.toFun x - (identityHarmonicReplacementDatum a m u hu).v.toFun x) ≤ C * scalarIdentityWeakError a b m * Book.Ch03.h1EnergyNormOnCube (originCube d m) a u

The normalized L² distance to the identity-harmonic same-trace replacement is controlled by the response error at any prescribed positive order below one half.