High-contrast homogenization: Provider.Regularity.ObservationCoefficientTransport

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

Observation-cube coefficient and equation transport

A physical weak solution is restricted to an inward cube and pulled back by translation to the origin cube of the same scale. A representative of the source coefficient that is elliptic at every point of every ball, with that ball's own constants, is translated and packaged as a Chapter 3 coefficient family.

theorem HCPolySupport.HighContrast.IsWeakSolutionOn.untranslate {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {F : Vec d → Vec d} (z : Vec d) (h : IsWeakSolutionOn b (translateSet z U) F) : IsWeakSolutionOn (translateCoeffField z b) U fun (x : Vec d) => F (x + z)

Pull a smooth-test weak equation on a translated domain back to the untranslated domain.

theorem HCPolySupport.HighContrast.exists_observationCoeffFamily_and_forcedEquation {d : ℕ} {U : Set (Vec d)} (aSource : Source.AKL.Field d) (haSource : AEUniformlyEllipticField aSource) (aPhysical : CoeffField d) (haeSource : ↑aSource =ᵐ[MeasureTheory.volume] aPhysical) (u : H1Function U) (huPhysical : IsWeakSolutionOn aPhysical U u.grad) (center : Vec d) (m : ℤ) (hobs : Book.Ch03.openCubeAtScale center m ⊆ U) : ∃ (aObs : Book.Ch03.CoeffFamily d) (uObs : H1Function (openCubeSet (originCube d m))), ((aObs.coeffOn (originCube d m)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => aPhysical (x + center)) ∧ (∀ (x : Vec d), uObs.toFun x = u.toFun (x + center)) ∧ (∀ (x : Vec d), uObs.grad x = u.grad (x + center)) ∧ Book.Ch03.IsForcedEquation (originCube d m) aObs uObs 0

Restrict a physical weak solution to an inward observation cube, pull it back to the origin, and package the translated source representative as a compatible coefficient family.