Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.HarmonicReplacement

High-contrast homogenization: Provider.Regularity.HarmonicReplacement #

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

Identity harmonic replacement on centered cubes #

This module selects the identity-coefficient harmonic comparison with the same boundary trace as a high-contrast weak solution. The quantitative estimates use the scale-separated Chapter 3 comparison theorem, so the response error is evaluated at a strictly lower order than the output norm.

source
noncomputable def HCPolySupport.HighContrast.identityHarmonicReplacementDatum {d : ℕ} (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.CoarseGrainingComparisonDatum (originCube d m) a (identityConstantCoeffMatrix d) 0

The chosen identity-coefficient harmonic comparison datum for a weak solution on a centered triadic cube.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.identityHarmonicReplacementDatum_u {d : ℕ} (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) :
    (identityHarmonicReplacementDatum a m u hu).u = u

    The solution component of the chosen comparison datum is the original weak solution.

    source
    theorem HCPolySupport.HighContrast.identityHarmonicReplacementDatum_characterization {d : ℕ} (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.IsConstantCoeffForcedEquation (originCube d m) (identityConstantCoeffMatrix d) (identityHarmonicReplacementDatum a m u hu).v 0 ∧ ∃ (w : H10Function (Book.Ch02.cubeDomain (originCube d m)).carrier), w.toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => u.toFun x - (identityHarmonicReplacementDatum a m u hu).v.toFun x

    The chosen replacement solves the identity-coefficient homogeneous weak equation and has the same boundary trace as the original solution.