High-contrast homogenization: Provider.Regularity.CorrectorGlobalEquation

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

Globalizing compatible local weak equations

A compactly supported test lies in one member of the centered-cube exhaustion. A weak equation available on every exhaustion cube therefore gives the equation on all of Euclidean space.

theorem HCPolySupport.HighContrast.exists_localGradientCube_superset_of_isCompact {d : ℕ} {K : Set (Vec d)} (hK : IsCompact K) : ∃ (n : ℕ), K ⊆ localGradientCube d n

Every compact set lies in one centered cube of the exhaustion.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_univ_of_localGradientCube {d : ℕ} {b : CoeffField d} {F : Vec d → Vec d} (hlocal : ∀ (n : ℕ), IsWeakSolutionOn b (localGradientCube d n) F) : IsWeakSolutionOn b Set.univ F

Weak equations on every centered exhaustion cube globalize to the whole space, since each test function has compact support.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_of_isAHarmonicGradient {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {lam Lam : ℝ} (hU : IsOpen U) (hEll : IsEllipticFieldOn lam Lam U b) (u : H1Function U) (hu : IsAHarmonicGradient b U u.grad) : IsWeakSolutionOn b U u.grad

An H1Function whose gradient is coefficient-harmonic satisfies the project's weak-solution predicate.

theorem HCPolySupport.HighContrast.IsWeakSolutionOn.congr_ae {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} {F G : Vec d → Vec d} (hab : a =ᵐ[MeasureTheory.volume.restrict U] b) (hFG : F =ᵐ[MeasureTheory.volume.restrict U] G) (h : IsWeakSolutionOn a U F) : IsWeakSolutionOn b U G

The weak-solution predicate is invariant under a.e. replacement of both the coefficient and vector-field representatives.

theorem HCPolySupport.HighContrast.IsFiniteAffineCorrectionJointLocalEquation.isWeakSolutionOn_global {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {Phi : Vec d → NormalizedLocalH1Carrier d} (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) {b : CoeffField d} (hcoeff : ∀ (n : ℕ), Book.Ch03.publicCoeffField (originCube d ↑n) a =ᵐ[MeasureTheory.volume.restrict (localGradientCube d n)] b) (e : Vec d) : IsWeakSolutionOn b Set.univ fun (x : Vec d) => e + (Phi e).globalGradientRepresentative x

A joint local affine-corrector equation globalizes for any coefficient representative agreeing a.e. with every centered-cube public coefficient.