Measures on the subsets of the words, and invariant random subgroups

The upper approximation of the ergodic value (Main Theorem I (2), I:1170–1220) works with probability measures on {0,1}^B for finite sets B of words; their weak-* limits live on the compact space WordSpace = {0,1}^{words} of all subsets of the words (letters (i, e) with any i, unreduced). This file relates WordSpace to Sub(F), F the free group on s generators:

• wordEval s H, the words whose element of F lies in H, maps Sub(F) into WordSpace; it lands in the closed set Good s of subsets containing the empty word, invariant under cancelling a pair (i, c)(i, ¬c) and deleting a letter i ≥ s, and closed under u, v ↦ u v⁻¹ (Claim I:794 for words: these conditions are the paper's open cover of the complement);
• evW s A, the elements of F whose reduced word lies in A, maps Good s back to Sub(F) (isSubgroupIndicator_evW), as a left inverse of wordEval;
• conjW g is conjugation by a letter on WordSpace, intertwined with conj by wordEval.

irs_of_good is the transfer used at the limit: a probability measure on WordSpace carried by Good s and invariant under the conjW g (g a letter below s) is the image of an IRS with the same value. The value is valW, defined like valGen for a map to WordSpace.

The value through words

def MIPRE.Tailored.Sofic.Measure.litW (K : List SubgroupTestValue.Word) (A : SubgroupTestValue.Word → Bool) (lit : ℕ × Bool) : Bool

The literal (i, b) on a set of words.

Equations

• MIPRE.Tailored.Sofic.Measure.litW K A lit = match K[lit.1]? with | some k => A k == lit.2 | none => false

def MIPRE.Tailored.Sofic.Measure.passW (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) (A : SubgroupTestValue.Word → Bool) : Bool

A set of words passes the challenge (K, cl).

Equations

• MIPRE.Tailored.Sofic.Measure.passW K cl A = cl.any fun (c : List (ℕ × Bool)) => c.all fun (lit : ℕ × Bool) => MIPRE.Tailored.Sofic.Measure.litW K A lit

theorem MIPRE.Tailored.Sofic.Measure.passB_eq_passW (s : ℕ) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) (G : FreeGroup (Fin s) → Bool) : passB s K cl G = passW K cl fun (u : SubgroupTestValue.Word) => G (wordFG s u)

theorem MIPRE.Tailored.Sofic.Measure.passW_congr {K : List SubgroupTestValue.Word} (cl : List (List (ℕ × Bool))) {A B : SubgroupTestValue.Word → Bool} (h : ∀ k ∈ K, A k = B k) : passW K cl A = passW K cl B

passW depends only on the words of K.

theorem MIPRE.Tailored.Sofic.Measure.continuous_litW {X : Type u_1} [TopologicalSpace X] {e : X → SubgroupTestValue.Word → Bool} (he : Continuous e) (K : List SubgroupTestValue.Word) (lit : ℕ × Bool) : Continuous fun (x : X) => litW K (e x) lit

theorem MIPRE.Tailored.Sofic.Measure.continuous_passW {X : Type u_1} [TopologicalSpace X] {e : X → SubgroupTestValue.Word → Bool} (he : Continuous e) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : Continuous fun (x : X) => passW K cl (e x)

def MIPRE.Tailored.Sofic.Measure.passSetW {X : Type u_1} (e : X → SubgroupTestValue.Word → Bool) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : Set X

The set of points passing a challenge.

Equations

• MIPRE.Tailored.Sofic.Measure.passSetW e K cl = {x : X | MIPRE.Tailored.Sofic.Measure.passW K cl (e x) = true}

theorem MIPRE.Tailored.Sofic.Measure.isClopen_passSetW {X : Type u_1} [TopologicalSpace X] {e : X → SubgroupTestValue.Word → Bool} (he : Continuous e) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : IsClopen (passSetW e K cl)

noncomputable def MIPRE.Tailored.Sofic.Measure.valW {X : Type u_1} [MeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) (e : X → SubgroupTestValue.Word → Bool) (μ : MeasureTheory.ProbabilityMeasure X) : ℝ

The value of a probability measure on a space mapped to sets of words.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Sofic.Measure.valGen_eq_valW {X : Type u_1} [MeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) (ev : X → FreeGroup (Fin T.nGen) → Bool) (μ : MeasureTheory.ProbabilityMeasure X) : valGen T ev μ = valW T (fun (x : X) (u : SubgroupTestValue.Word) => ev x (wordFG T.nGen u)) μ

theorem MIPRE.Tailored.Sofic.Measure.continuous_valW {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) {e : X → SubgroupTestValue.Word → Bool} (he : Continuous e) : Continuous (valW T e)

theorem MIPRE.Tailored.Sofic.Measure.valW_map {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [TopologicalSpace Y] [OpensMeasurableSpace Y] (T : SubgroupTestValue.SubgroupTestData) {e : Y → SubgroupTestValue.Word → Bool} (he : Continuous e) {f : X → Y} (hf : Measurable f) (μ : MeasureTheory.ProbabilityMeasure X) : valW T e (μ.map f) = valW T (e ∘ f) μ

The value is unchanged along a measurable map.

theorem MIPRE.Tailored.Sofic.Measure.valW_congr_ae {X : Type u_1} [MeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) {e e' : X → SubgroupTestValue.Word → Bool} (μ : MeasureTheory.ProbabilityMeasure X) (h : ∀ᵐ (x : X) ∂↑μ, e x = e' x) : valW T e μ = valW T e' μ

The value only sees the passing sets up to null sets.

The space of sets of words

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Measure.WordSpace : Type

The sets of words, {0,1}^{words} with the product topology.

Equations

• MIPRE.Tailored.Sofic.Measure.WordSpace = (SubgroupTestValue.Word → Bool)

noncomputable def MIPRE.Tailored.Sofic.Measure.valΩ (T : SubgroupTestValue.SubgroupTestData) (ν : MeasureTheory.ProbabilityMeasure WordSpace) : ℝ

The value of a probability measure on sets of words.

Equations

• MIPRE.Tailored.Sofic.Measure.valΩ T ν = MIPRE.Tailored.Sofic.Measure.valW T id ν

theorem MIPRE.Tailored.Sofic.Measure.continuous_valΩ (T : SubgroupTestValue.SubgroupTestData) : Continuous (valΩ T)

Words and the free group

theorem MIPRE.Tailored.Sofic.Measure.wordFG_append (s : ℕ) (u v : SubgroupTestValue.Word) : wordFG s (u ++ v) = wordFG s u * wordFG s v

theorem MIPRE.Tailored.Sofic.Measure.wordFG_cons (s : ℕ) (l : SubgroupTestValue.Letter) (u : SubgroupTestValue.Word) : wordFG s (l :: u) = letterFG s l * wordFG s u

theorem MIPRE.Tailored.Sofic.Measure.wordFG_nil (s : ℕ) : wordFG s [] = 1

theorem MIPRE.Tailored.Sofic.Measure.letterFG_flip (s : ℕ) (l : SubgroupTestValue.Letter) : letterFG s (l.1, !l.2) = (letterFG s l)⁻¹

theorem MIPRE.Tailored.Sofic.Measure.wordFG_invW (s : ℕ) (u : SubgroupTestValue.Word) : wordFG s (invW u) = (wordFG s u)⁻¹

theorem MIPRE.Tailored.Sofic.Measure.letterFG_of_le {s : ℕ} {l : SubgroupTestValue.Letter} (h : s ≤ l.1) : letterFG s l = 1

def MIPRE.Tailored.Sofic.Measure.toN (s : ℕ) (x : Fin s × Bool) : SubgroupTestValue.Letter

A letter of the free group as a letter of a word (Mathlib's true is the generator, the words' true its inverse).

Equations

• MIPRE.Tailored.Sofic.Measure.toN s x = (↑x.1, !x.2)

def MIPRE.Tailored.Sofic.Measure.finW (s : ℕ) (w : SubgroupTestValue.Word) : List (Fin s × Bool)

The letters of a word below s, as a word of the free group.

Equations

• MIPRE.Tailored.Sofic.Measure.finW s w = List.filterMap (fun (l : SubgroupTestValue.Letter) => if h : l.1 < s then some (⟨l.1, h⟩, !l.2) else none) w

theorem MIPRE.Tailored.Sofic.Measure.wordFG_eq_mk (s : ℕ) (w : SubgroupTestValue.Word) : wordFG s w = FreeGroup.mk (finW s w)

theorem MIPRE.Tailored.Sofic.Measure.finW_map_toN (s : ℕ) (L : List (Fin s × Bool)) : finW s (List.map (toN s) L) = L

def MIPRE.Tailored.Sofic.Measure.toWordN (s : ℕ) (g : FreeGroup (Fin s)) : SubgroupTestValue.Word

The word of an element of the free group.

Equations

• MIPRE.Tailored.Sofic.Measure.toWordN s g = List.map (MIPRE.Tailored.Sofic.Measure.toN s) g.toWord

theorem MIPRE.Tailored.Sofic.Measure.wordFG_toWordN (s : ℕ) (g : FreeGroup (Fin s)) : wordFG s (toWordN s g) = g

theorem MIPRE.Tailored.Sofic.Measure.map_toN_invRev (s : ℕ) (L : List (Fin s × Bool)) : List.map (toN s) (FreeGroup.invRev L) = invW (List.map (toN s) L)

Subgroups as sets of words

def MIPRE.Tailored.Sofic.Measure.wordEval (s : ℕ) (H : SubgroupTestValue.SubgroupSpace s) : WordSpace

The words whose element of the free group lies in H.

Equations

• MIPRE.Tailored.Sofic.Measure.wordEval s H u = ↑H (MIPRE.Tailored.Sofic.Measure.wordFG s u)

theorem MIPRE.Tailored.Sofic.Measure.continuous_wordEval (s : ℕ) : Continuous (wordEval s)

theorem MIPRE.Tailored.Sofic.Measure.measurable_wordEval (s : ℕ) : Measurable (wordEval s)

def MIPRE.Tailored.Sofic.Measure.Good (s : ℕ) : Set WordSpace

The sets of words that come from subgroups, by local conditions.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.Sofic.Measure.wordEval_mem_good {s : ℕ} (H : SubgroupTestValue.SubgroupSpace s) : wordEval s H ∈ Good s

theorem MIPRE.Tailored.Sofic.Measure.good_red {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) {L₁ L₂ : List (Fin s × Bool)} (h : FreeGroup.Red L₁ L₂) : A (List.map (toN s) L₁) = A (List.map (toN s) L₂)

theorem MIPRE.Tailored.Sofic.Measure.evW_mk {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) (L : List (Fin s × Bool)) : A (List.map (toN s) (FreeGroup.mk L).toWord) = A (List.map (toN s) L)

On Good s, the value of the element of a word of the free group is the value of the word.

theorem MIPRE.Tailored.Sofic.Measure.good_filter {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) (u₁ u : SubgroupTestValue.Word) : A (u₁ ++ u) = A (u₁ ++ List.map (toN s) (finW s u))

def MIPRE.Tailored.Sofic.Measure.evW (s : ℕ) (A : WordSpace) : FreeGroup (Fin s) → Bool

The elements of the free group whose reduced word lies in A.

Equations

• MIPRE.Tailored.Sofic.Measure.evW s A g = A (MIPRE.Tailored.Sofic.Measure.toWordN s g)

theorem MIPRE.Tailored.Sofic.Measure.continuous_evW (s : ℕ) : Continuous (evW s)

theorem MIPRE.Tailored.Sofic.Measure.evW_wordFG {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) (u : SubgroupTestValue.Word) : evW s A (wordFG s u) = A u

theorem MIPRE.Tailored.Sofic.Measure.isSubgroupIndicator_evW {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) : SubgroupTestValue.IsSubgroupIndicator (evW s A)

theorem MIPRE.Tailored.Sofic.Measure.evW_wordEval {s : ℕ} (H : SubgroupTestValue.SubgroupSpace s) : evW s (wordEval s H) = ↑H

Conjugation by a letter

def MIPRE.Tailored.Sofic.Measure.conjW (g : SubgroupTestValue.Letter) (A : WordSpace) : WordSpace

Conjugation by a letter on sets of words: u ∈ conjW g A when g⁻¹ u g ∈ A.

Equations

• MIPRE.Tailored.Sofic.Measure.conjW g A u = A (MIPRE.Tailored.Sofic.invW [g] ++ u ++ [g])

theorem MIPRE.Tailored.Sofic.Measure.continuous_conjW (g : SubgroupTestValue.Letter) : Continuous (conjW g)

theorem MIPRE.Tailored.Sofic.Measure.measurable_conjW (g : SubgroupTestValue.Letter) : Measurable (conjW g)

theorem MIPRE.Tailored.Sofic.Measure.wordEval_conj {s : ℕ} (g : SubgroupTestValue.Letter) (H : SubgroupTestValue.SubgroupSpace s) : wordEval s (SubgroupTestValue.conj (letterFG s g) H) = conjW g (wordEval s H)

theorem MIPRE.Tailored.Sofic.Measure.evW_conjW {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) (g : SubgroupTestValue.Letter) : evW s (conjW g A) = fun (v : FreeGroup (Fin s)) => evW s A ((letterFG s g)⁻¹ * v * letterFG s g)

From measures on words to invariant random subgroups

def MIPRE.Tailored.Sofic.Measure.badSet (s : ℕ) : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool → Set WordSpace

The bad sets: the complement of Good s is their union.

Equations

• MIPRE.Tailored.Sofic.Measure.badSet s (Sum.inl val) = {A : MIPRE.Tailored.Sofic.Measure.WordSpace | A [] = false}
• MIPRE.Tailored.Sofic.Measure.badSet s (Sum.inr (Sum.inl (u₁, u₂, i, c))) = {A : MIPRE.Tailored.Sofic.Measure.WordSpace | A (u₁ ++ (i, c) :: (i, !c) :: u₂) ≠ A (u₁ ++ u₂)}
• MIPRE.Tailored.Sofic.Measure.badSet s (Sum.inr (Sum.inr (Sum.inl (u, v)))) = {A : MIPRE.Tailored.Sofic.Measure.WordSpace | A u = true ∧ A v = true ∧ A (u ++ MIPRE.Tailored.Sofic.invW v) = false}
• MIPRE.Tailored.Sofic.Measure.badSet s (Sum.inr (Sum.inr (Sum.inr (u₁, u₂, i, c)))) = {A : MIPRE.Tailored.Sofic.Measure.WordSpace | s ≤ i ∧ A (u₁ ++ (i, c) :: u₂) ≠ A (u₁ ++ u₂)}

theorem MIPRE.Tailored.Sofic.Measure.compl_good (s : ℕ) : (Good s)ᶜ = ⋃ (b : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool), badSet s b

theorem MIPRE.Tailored.Sofic.Measure.isClopen_badSet (s : ℕ) (b : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool) : IsClopen (badSet s b)

theorem MIPRE.Tailored.Sofic.Measure.measurableSet_good (s : ℕ) : MeasurableSet (Good s)

instance MIPRE.Tailored.Sofic.Measure.instCountableFreeGroupFin_mIPRE (s : ℕ) : Countable (FreeGroup (Fin s))

theorem MIPRE.Tailored.Sofic.Measure.measurableSpace_subgroupSpace (s : ℕ) : SubgroupTestValue.instMeasurableSpaceSubgroupSpace s = MeasurableSpace.comap (fun (H : SubgroupTestValue.SubgroupSpace s) => ↑H) inferInstance

The measurable structure of Sub(F) is the one induced from the indicators.

theorem MIPRE.Tailored.Sofic.Measure.measurable_to_subgroupSpace {X : Type u_1} [MeasurableSpace X] {s : ℕ} {f : X → SubgroupTestValue.SubgroupSpace s} (hf : Measurable fun (x : X) => ↑(f x)) : Measurable f

noncomputable def MIPRE.Tailored.Sofic.Measure.toSub (s : ℕ) (A : WordSpace) : SubgroupTestValue.SubgroupSpace s

The subgroup of a good set of words; the whole group otherwise.

Equations

• MIPRE.Tailored.Sofic.Measure.toSub s A = ⟨if A ∈ MIPRE.Tailored.Sofic.Measure.Good s then MIPRE.Tailored.Sofic.Measure.evW s A else fun (x : FreeGroup (Fin s)) => true, ⋯⟩

theorem MIPRE.Tailored.Sofic.Measure.toSub_of_good {s : ℕ} {A : WordSpace} (hA : A ∈ Good s) : ↑(toSub s A) = evW s A

theorem MIPRE.Tailored.Sofic.Measure.measurable_toSub (s : ℕ) : Measurable (toSub s)

theorem MIPRE.Tailored.Sofic.Measure.conj_mul {s : ℕ} (w₁ w₂ : FreeGroup (Fin s)) (H : SubgroupTestValue.SubgroupSpace s) : SubgroupTestValue.conj (w₁ * w₂) H = SubgroupTestValue.conj w₁ (SubgroupTestValue.conj w₂ H)

theorem MIPRE.Tailored.Sofic.Measure.conj_one {s : ℕ} (H : SubgroupTestValue.SubgroupSpace s) : SubgroupTestValue.conj 1 H = H

theorem MIPRE.Tailored.Sofic.Measure.irs_of_good (T : SubgroupTestValue.SubgroupTestData) (ν : MeasureTheory.ProbabilityMeasure WordSpace) (hG : ↑ν (Good T.nGen)ᶜ = 0) (hinv : ∀ (g : SubgroupTestValue.Letter), g.1 < T.nGen → MeasureTheory.Measure.map (conjW g) ↑ν = ↑ν) : ∃ μ ∈ SubgroupTestValue.IRS T.nGen, T.valOn μ = valΩ T ν

The transfer to Sub(F): a probability measure on sets of words carried by Good s and invariant under conjugation by the letters below s is the image of an IRS with the same value.

theorem MIPRE.Tailored.Sofic.Measure.map_wordEval_conjW {s : ℕ} {μ : MeasureTheory.ProbabilityMeasure (SubgroupTestValue.SubgroupSpace s)} (hμ : μ ∈ SubgroupTestValue.IRS s) (g : SubgroupTestValue.Letter) : MeasureTheory.Measure.map (conjW g) (MeasureTheory.Measure.map (wordEval s) ↑μ) = MeasureTheory.Measure.map (wordEval s) ↑μ

The image of an IRS on sets of words is invariant under conjugation by the letters.

theorem MIPRE.Tailored.Sofic.Measure.valOn_eq_valΩ (T : SubgroupTestValue.SubgroupTestData) (μ : MeasureTheory.ProbabilityMeasure (SubgroupTestValue.SubgroupSpace T.nGen)) : T.valOn μ = valΩ T (μ.map (wordEval T.nGen))

The value of a measure on Sub(F) is the value of its image on sets of words.