High-contrast homogenization: Provider.Quenched.InvariantFullMeasureEventAE

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

Invariant full-measure events from almost-everywhere properties

An almost-everywhere property need not itself define a measurable set. Its failure set nevertheless has outer measure zero, hence admits a measurable null superset. The complement is a measurable full-measure subset on which the property holds pointwise, and the integer-translation invariant core can then be applied without any measurability hypothesis on the property.

theorem HCPolySupport.HighContrast.Quenched.exists_integerTranslate_invariant_fullMeasure_of_ae {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsStationaryLaw P) {Good : CoeffSpace d → Prop} (hGood : ∀ᵐ (a : CoeffSpace d) ∂P, Good a) : ∃ (Ωend : Set (CoeffSpace d)), MeasurableSet Ωend ∧ P.real Ωend = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' Ωend = Ωend) ∧ ∀ a ∈ Ωend, Good a

An almost-everywhere property under a stationary probability law holds on a measurable, literally integer-translation invariant probability-one event. No measurability assumption on the property is required.