High-contrast homogenization: Frozen.Stationarity

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

Stationarity of the coefficient law

The law of the coefficient field is invariant under the integer translations of the coefficient space. The coefficient fields are uniformly elliptic almost everywhere, with ellipticity constants belonging to the field and entering no estimate; e.qualitative.ellipticity follows from this, and every quantitative object of the development — Π, the gauge and its growth witness, Θ_m, and every dimensional constant — is independent of them.

def HCPoly.Frozen.IsStationaryLaw {d : ℕ} (P : MeasureTheory.Measure (HCPolySupport.HighContrast.CoeffSpace d)) : Prop

Stationarity of the coefficient law. Every integer translation of the coefficient space preserves the law.

Equations

• HCPoly.Frozen.IsStationaryLaw P = ∀ (z : Fin d → ℤ), MeasureTheory.Measure.map (HCPolySupport.HighContrast.translateCoeff z) P = P

The assumption under the project namespace

HCPolySupport.HighContrast.IsStationaryLaw is HCPoly.Frozen.IsStationaryLaw itself, not a second reading of it: the proofs of the paper's propositions are written in the project namespace and use the frozen declaration through this name.