High-contrast homogenization: Provider.Regularity.CorrectorInvariantEvent

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

The invariant full-measure event of the coefficient space

The integer translations act on the coefficient space as a group, and the intersection of all their preimages of a full-measure measurable event is again a measurable full-measure event, this time invariant under every integer translation. This is the event on which one common corrector family can be defined for all phases at once.

The integer translation group action

theorem HCPolySupport.HighContrast.intTranslation_add {d : ℕ} (z w : Fin d → ℤ) : Source.AKL.intTranslation (z + w) = Source.AKL.intTranslation z + Source.AKL.intTranslation w

The translation vector of a sum of integer vectors splits.

theorem HCPolySupport.HighContrast.intTranslation_zero {d : ℕ} : Source.AKL.intTranslation 0 = 0

The translation vector of the zero integer vector vanishes.

theorem HCPolySupport.HighContrast.translateField_zero {d : ℕ} (a : Source.AKL.Field d) : Source.AKL.translateField 0 a = a

Translating a field by zero leaves it unchanged.

theorem HCPolySupport.HighContrast.translateField_translateField {d : ℕ} (z w : Fin d → ℤ) (a : Source.AKL.Field d) : Source.AKL.translateField z (Source.AKL.translateField w a) = Source.AKL.translateField (z + w) a

Successive field translations compose.

@[simp]

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

Translating a coefficient sample by zero leaves it unchanged.

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

Successive coefficient translations compose.

The invariant core of an event

def HCPolySupport.HighContrast.invariantTranslationCore {d : ℕ} (G : Set (CoeffSpace d)) : Set (CoeffSpace d)

The integer-translation invariant core of an event: the samples all of whose integer translates lie in the event.

Equations

• HCPolySupport.HighContrast.invariantTranslationCore G = ⋂ (z : Fin d → ℤ), HCPolySupport.HighContrast.translateCoeff z ⁻¹' G

theorem HCPolySupport.HighContrast.mem_invariantTranslationCore_iff {d : ℕ} {G : Set (CoeffSpace d)} {a : CoeffSpace d} : a ∈ invariantTranslationCore G ↔ ∀ (z : Fin d → ℤ), translateCoeff z a ∈ G

theorem HCPolySupport.HighContrast.preimage_translateCoeff_invariantTranslationCore {d : ℕ} (G : Set (CoeffSpace d)) (z : Fin d → ℤ) : translateCoeff z ⁻¹' invariantTranslationCore G = invariantTranslationCore G

The invariant core is invariant under every integer translation.

Full measure under a stationary law