The value of a subgroup test as a weak-* continuous functional

Paper I, I:439–460: the value val(T, π) of a test against a probability measure π on the subsets of the free group is the probability that a subset drawn from π passes a challenge drawn with probability proportional to its weight. A challenge depends on finitely many coordinates of the subset, so its passing set is clopen and the value is weak-* continuous.

The value is defined here for a measure on any space X with a continuous map ev to the indicator functions FreeGroup (Fin s) → Bool (valGen); SubgroupTestData.valOn is the case X = Sub(F), ev = Subtype.val, and the upper approximation of the ergodic value uses the case X = {0,1}^F. The main results:

• wordFG: the element of the free group of a word, its letters beyond the generators dropped, with FreeGroup.lift σ.σ (wordFG w) = σ.wordPerm w (lift_wordFG);
• continuous_valGen, SubgroupTestData.continuous_valOn: weak-* continuity;
• SubgroupTestData.valOn_finDesc: on the finitely described IRS Φ(σ) the value is T.value σ.

Words as elements of the free group

def MIPRE.Tailored.Sofic.Measure.letterFG (s : ℕ) (l : SubgroupTestValue.Letter) : FreeGroup (Fin s)

The element of the free group of a letter; a letter beyond the s generators is the identity, as in FiniteAction.letterPerm.

Equations

• MIPRE.Tailored.Sofic.Measure.letterFG s l = if h : l.1 < s then if l.2 = true then (FreeGroup.of ⟨l.1, h⟩)⁻¹ else FreeGroup.of ⟨l.1, h⟩ else 1

def MIPRE.Tailored.Sofic.Measure.wordFG (s : ℕ) (w : SubgroupTestValue.Word) : FreeGroup (Fin s)

The element of the free group of a word, the product of its letters from left to right.

Equations

• MIPRE.Tailored.Sofic.Measure.wordFG s w = (List.map (MIPRE.Tailored.Sofic.Measure.letterFG s) w).prod

theorem MIPRE.Tailored.Sofic.Measure.lift_letterFG {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) (l : SubgroupTestValue.Letter) : (FreeGroup.lift σ.σ) (letterFG s l) = σ.letterPerm l

theorem MIPRE.Tailored.Sofic.Measure.lift_wordFG {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) (w : SubgroupTestValue.Word) : (FreeGroup.lift σ.σ) (wordFG s w) = σ.wordPerm w

A finite action's permutation of a word is the image of the word's element of the free group.

theorem MIPRE.Tailored.Sofic.Measure.stab_wordFG {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) (x : Fin σ.N) (w : SubgroupTestValue.Word) : ↑(SubgroupTestValue.stab σ x) (wordFG s w) = decide (σ.InStab x w)

Membership of a word in a stabilizer, through the free group.

Passing a challenge

def MIPRE.Tailored.Sofic.Measure.litB (s : ℕ) (K : List SubgroupTestValue.Word) (A : FreeGroup (Fin s) → Bool) (lit : ℕ × Bool) : Bool

The literal (i, b) on an indicator A: the i-th word of K lies in A exactly when b; false when i is beyond K.

Equations

• MIPRE.Tailored.Sofic.Measure.litB s K A lit = match K[lit.1]? with | some k => A (MIPRE.Tailored.Sofic.Measure.wordFG s k) == lit.2 | none => false

def MIPRE.Tailored.Sofic.Measure.passB (s : ℕ) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) (A : FreeGroup (Fin s) → Bool) : Bool

The indicator A passes the challenge (K, clauses): some clause holds.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.litB_stab {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) (x : Fin σ.N) (K : List SubgroupTestValue.Word) (lit : ℕ × Bool) : litB s K (↑(SubgroupTestValue.stab σ x)) lit = decide (σ.LitHolds K x lit)

theorem MIPRE.Tailored.Sofic.Measure.passB_stab {s : ℕ} (σ : SubgroupTestValue.FiniteAction s) (x : Fin σ.N) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : passB s K cl ↑(SubgroupTestValue.stab σ x) = decide (σ.Passes K cl x)

Continuity

theorem MIPRE.Tailored.Sofic.Measure.continuous_bool_and {X : Type u_1} [TopologicalSpace X] {f g : X → Bool} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => f x && g x

theorem MIPRE.Tailored.Sofic.Measure.continuous_bool_or {X : Type u_1} [TopologicalSpace X] {f g : X → Bool} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => f x || g x

theorem MIPRE.Tailored.Sofic.Measure.continuous_list_all {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} (l : List ι) (f : ι → X → Bool) (h : ∀ i ∈ l, Continuous (f i)) : Continuous fun (x : X) => l.all fun (i : ι) => f i x

theorem MIPRE.Tailored.Sofic.Measure.continuous_list_any {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} (l : List ι) (f : ι → X → Bool) (h : ∀ i ∈ l, Continuous (f i)) : Continuous fun (x : X) => l.any fun (i : ι) => f i x

theorem MIPRE.Tailored.Sofic.Measure.continuous_litB {X : Type u_1} [TopologicalSpace X] {s : ℕ} {ev : X → FreeGroup (Fin s) → Bool} (hev : Continuous ev) (K : List SubgroupTestValue.Word) (lit : ℕ × Bool) : Continuous fun (x : X) => litB s K (ev x) lit

theorem MIPRE.Tailored.Sofic.Measure.continuous_passB {X : Type u_1} [TopologicalSpace X] {s : ℕ} {ev : X → FreeGroup (Fin s) → Bool} (hev : Continuous ev) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : Continuous fun (x : X) => passB s K cl (ev x)

def MIPRE.Tailored.Sofic.Measure.passSet {X : Type u_1} (s : ℕ) (ev : X → FreeGroup (Fin s) → Bool) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : Set X

The set of points passing a challenge.

Equations

• MIPRE.Tailored.Sofic.Measure.passSet s ev K cl = {x : X | MIPRE.Tailored.Sofic.Measure.passB s K cl (ev x) = true}

theorem MIPRE.Tailored.Sofic.Measure.isClopen_passSet {X : Type u_1} [TopologicalSpace X] {s : ℕ} {ev : X → FreeGroup (Fin s) → Bool} (hev : Continuous ev) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : IsClopen (passSet s ev K cl)

theorem MIPRE.Tailored.Sofic.Measure.continuous_measureReal_of_isClopen {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {E : Set X} (hE : IsClopen E) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => (↑μ).real E

The measure of a clopen set is weak-* continuous.

The value

noncomputable def MIPRE.Tailored.Sofic.Measure.valGen {X : Type u_1} [MeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) (ev : X → FreeGroup (Fin T.nGen) → Bool) (μ : MeasureTheory.ProbabilityMeasure X) : ℝ

The value val(T, μ) (I:455) of a probability measure on a space X mapped continuously to the indicators: the weighted measure of the sets passing each challenge, normalized by the total weight as in SubgroupTestData.value.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.continuous_list_sum_map {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (l : List ι) (f : ι → X → ℝ) (h : ∀ i ∈ l, Continuous (f i)) : Continuous fun (x : X) => (List.map (fun (i : ι) => f i x) l).sum

theorem MIPRE.Tailored.Sofic.Measure.continuous_valGen {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) {ev : X → FreeGroup (Fin T.nGen) → Bool} (hev : Continuous ev) : Continuous (valGen T ev)

The value is weak- continuous.*

theorem MIPRE.Tailored.Sofic.Measure.valGen_nonneg {X : Type u_1} [MeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) (ev : X → FreeGroup (Fin T.nGen) → Bool) (μ : MeasureTheory.ProbabilityMeasure X) : 0 ≤ valGen T ev μ

theorem MIPRE.Tailored.Sofic.Measure.weighted_le_one {ι : Type u_1} (l : List (ℕ × ι)) (p : ι → ℝ) (hp : ∀ c ∈ l, p c.2 ≤ 1) : (List.map (fun (c : ℕ × ι) => ↑c.1 * p c.2) l).sum ≤ ↑(List.map (fun (x : ℕ × ι) => x.1) l).sum

A weighted average of numbers in [0, 1] is at most 1.

theorem MIPRE.Tailored.Sofic.Measure.valGen_le_one {X : Type u_1} [MeasurableSpace X] (T : SubgroupTestValue.SubgroupTestData) (ev : X → FreeGroup (Fin T.nGen) → Bool) (μ : MeasureTheory.ProbabilityMeasure X) : valGen T ev μ ≤ 1

noncomputable def SubgroupTestValue.FiniteAction.finDesc {s : ℕ} (σ : FiniteAction s) : MeasureTheory.ProbabilityMeasure (SubgroupSpace s)

The finitely described IRS Φ(σ) (I:510) as a probability measure.

Equations

• σ.finDesc = ⟨(↑σ.N)⁻¹ • ∑ x : Fin σ.N, MeasureTheory.Measure.dirac (SubgroupTestValue.stab σ x), ⋯⟩

theorem SubgroupTestValue.FiniteAction.finDesc_mem {s : ℕ} (σ : FiniteAction s) : σ.finDesc ∈ finDescIRS s

theorem SubgroupTestValue.FiniteAction.measureReal_eq {s : ℕ} (σ : FiniteAction s) (μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace s)) (hμ : ↑μ = (↑σ.N)⁻¹ • ∑ x : Fin σ.N, MeasureTheory.Measure.dirac (stab σ x)) {E : Set (SubgroupSpace s)} (hE : MeasurableSet E) : (↑μ).real E = ↑{x : Fin σ.N | stab σ x ∈ E}.card / ↑σ.N

The measure of a measurable set under Φ(σ): the fraction of the points whose stabilizer it contains.

def SubgroupTestValue.SubgroupTestData.subVal (s : ℕ) (H : SubgroupSpace s) : FreeGroup (Fin s) → Bool

The indicator of a subgroup.

Equations

• SubgroupTestValue.SubgroupTestData.subVal s H = ↑H

theorem SubgroupTestValue.SubgroupTestData.continuous_subVal (s : ℕ) : Continuous (subVal s)

noncomputable def SubgroupTestValue.SubgroupTestData.valOn (T : SubgroupTestData) (μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace T.nGen)) : ℝ

The value of a probability measure on Sub(F) (I:455): the weighted measure of the set of subgroups passing each challenge, normalized as in value.

Equations

• T.valOn μ = MIPRE.Tailored.Sofic.Measure.valGen T (SubgroupTestValue.SubgroupTestData.subVal T.nGen) μ

theorem SubgroupTestValue.SubgroupTestData.continuous_valOn (T : SubgroupTestData) : Continuous T.valOn

The value is weak- continuous* (I:458).

theorem SubgroupTestValue.SubgroupTestData.valOn_nonneg (T : SubgroupTestData) (μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace T.nGen)) : 0 ≤ T.valOn μ

theorem SubgroupTestValue.SubgroupTestData.valOn_le_one (T : SubgroupTestData) (μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace T.nGen)) : T.valOn μ ≤ 1

theorem SubgroupTestValue.SubgroupTestData.valOn_of_eq (T : SubgroupTestData) (σ : FiniteAction T.nGen) (μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace T.nGen)) (hμ : ↑μ = (↑σ.N)⁻¹ • ∑ x : Fin σ.N, MeasureTheory.Measure.dirac (stab σ x)) : T.valOn μ = T.value σ

The value of a finitely described IRS Φ(σ) is the value of σ.

theorem SubgroupTestValue.SubgroupTestData.valOn_finDesc (T : SubgroupTestData) (σ : FiniteAction T.nGen) : T.valOn σ.finDesc = T.value σ

theorem SubgroupTestValue.SubgroupTestData.value_nonneg (T : SubgroupTestData) (σ : FiniteAction T.nGen) : 0 ≤ T.value σ

theorem SubgroupTestValue.SubgroupTestData.value_le_one (T : SubgroupTestData) (σ : FiniteAction T.nGen) : T.value σ ≤ 1