High-contrast homogenization: Provider.Quenched.InvariantFullMeasureEvent

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

Integer-translation invariant full-measure events

This file constructs the literal invariant event used in the quenched endgame. Starting from one measurable full-measure event, it intersects all of its integer translates. The resulting event is a measurable, full-measure, translation-invariant subset of the original event.

theorem HCPolySupport.HighContrast.Quenched.translateCoeff_add {d : ℕ} (z w : Fin d → ℤ) (a : CoeffSpace d) : translateCoeff z (translateCoeff w a) = translateCoeff (z + w) a

Integer translations of coefficient fields compose additively.

theorem HCPolySupport.HighContrast.Quenched.translateCoeff_zero {d : ℕ} (a : CoeffSpace d) : translateCoeff 0 a = a

Translation by the zero integer vector fixes every coefficient field.

theorem HCPolySupport.HighContrast.Quenched.exists_integerTranslate_invariant_fullMeasure_subset {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsStationaryLaw P) {Ωgood : Set (CoeffSpace d)} (hΩgood : MeasurableSet Ωgood) (hΩgood_full : P.real Ωgood = 1) : ∃ (Ωend : Set (CoeffSpace d)), MeasurableSet Ωend ∧ P.real Ωend = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' Ωend = Ωend) ∧ Ωend ⊆ Ωgood

Every measurable full-measure event contains a measurable full-measure subevent that is literally invariant under all integer translations.