Limits of approximately good, approximately invariant measures

Paper I, the proof of Main Theorem I (2), second half (I:1204–1217): a weak-* limit of points of the polytopes Q̃_{B_t} is an IRS. Here: if probability measures ν t on sets of words give eventually no mass to each bad set and are eventually invariant, up to any η > 0, on each cylinder restrSet J q under conjugation by each letter below s, then their values are eventually at most valErg + ε (eventually_valΩ_le). The probability measures on the compact space WordSpace form a compact space (Prokhorov, in Mathlib), so a frequently bad subsequence would have a cluster point; it is carried by Good s and invariant (the cylinders are a π-system generating the σ-algebra), so it is the image of an IRS (irs_of_good), whose value is at most the ergodic value.

def MIPRE.Tailored.Sofic.Measure.cylinders : Set (Set WordSpace)

The cylinders.

Equations

• MIPRE.Tailored.Sofic.Measure.cylinders = {E : Set MIPRE.Tailored.Sofic.Measure.WordSpace | ∃ (J : List SubgroupTestValue.Word) (q : List Bool), E = MIPRE.Tailored.Sofic.Measure.restrSet J q}

theorem MIPRE.Tailored.Sofic.Measure.isPiSystem_cylinders : IsPiSystem cylinders

theorem MIPRE.Tailored.Sofic.Measure.generateFrom_cylinders : inferInstance = MeasurableSpace.generateFrom cylinders

theorem MIPRE.Tailored.Sofic.Measure.ext_cylinders {μ ν : MeasureTheory.Measure WordSpace} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : ∀ (J : List SubgroupTestValue.Word) (q : List Bool), μ (restrSet J q) = ν (restrSet J q)) : μ = ν

Two probability measures on sets of words agreeing on the cylinders are equal.

theorem MIPRE.Tailored.Sofic.Measure.isClopen_conjW_restrSet (g : SubgroupTestValue.Letter) (J : List SubgroupTestValue.Word) (q : List Bool) : IsClopen (conjW g ⁻¹' restrSet J q)

theorem MIPRE.Tailored.Sofic.Measure.mem_of_clusterPt {X : Type u_1} [TopologicalSpace X] {F : Filter ℕ} {ν : ℕ → X} {x : X} (hx : ClusterPt x (Filter.map ν F)) {S : Set X} (hS : IsClosed S) (h : ∀ᶠ (t : ℕ) in F, ν t ∈ S) : x ∈ S

A closed set eventually containing a sequence along a filter contains its cluster points.

theorem MIPRE.Tailored.Sofic.Measure.eventually_valΩ_le (T : SubgroupTestValue.SubgroupTestData) (ν : ℕ → MeasureTheory.ProbabilityMeasure WordSpace) (h1 : ∀ (b : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool), ∀ᶠ (t : ℕ) in Filter.atTop, ↑(ν t) (badSet T.nGen b) = 0) (h2 : ∀ (g : SubgroupTestValue.Letter), g.1 < T.nGen → ∀ (J : List SubgroupTestValue.Word) (q : List Bool), ∀ η > 0, ∀ᶠ (t : ℕ) in Filter.atTop, |(↑(ν t)).real (restrSet J q) - (↑(ν t)).real (conjW g ⁻¹' restrSet J q)| ≤ η) (ε : ℝ) : ε > 0 → ∀ᶠ (t : ℕ) in Filter.atTop, valΩ T (ν t) ≤ T.valErg + ε

Limits of approximately good, approximately invariant measures: their values are eventually at most the ergodic value plus any ε > 0.