The ergodic value, and the sofic value under the Aldous–Lyons conjecture

Paper I, I:497 and Corollary I:550. The ergodic value valErg T of a test is the supremum of its value over the invariant random subgroups. The finitely described IRSs are invariant (finDescIRS_subset_IRS), so the sofic value is at most the ergodic value (valSof_le_valErg). Under the Aldous–Lyons conjecture they are equal (valSof_eq_valErg): the finitely described IRSs are dense in the IRSs and the value is weak-* continuous.

Conjugation

theorem SubgroupTestValue.continuous_conj {s : ℕ} (w : FreeGroup (Fin s)) : Continuous (conj w)

theorem SubgroupTestValue.measurable_conj {s : ℕ} (w : FreeGroup (Fin s)) : Measurable (conj w)

theorem SubgroupTestValue.conj_stab {s : ℕ} (σ : FiniteAction s) (w : FreeGroup (Fin s)) (x : Fin σ.N) : conj w (stab σ x) = stab σ (((FreeGroup.lift σ.σ) w) x)

Conjugating a stabilizer: w Stab(σ, x) w⁻¹ = Stab(σ, σ(w) x).

theorem SubgroupTestValue.finDescIRS_subset_IRS (s : ℕ) : finDescIRS s ⊆ IRS s

The finitely described IRSs are invariant.

def SubgroupTestValue.FiniteAction.trivial (s : ℕ) : FiniteAction s

The trivial action on one point.

Equations

• SubgroupTestValue.FiniteAction.trivial s = { N := 1, N_pos := SubgroupTestValue.FiniteAction.trivial._proof_1, σ := fun (x : Fin s) => 1 }

instance SubgroupTestValue.FiniteAction.instNonempty (s : ℕ) : Nonempty (FiniteAction s)

theorem SubgroupTestValue.FiniteAction.finDesc_mem_IRS {s : ℕ} (σ : FiniteAction s) : σ.finDesc ∈ IRS s

noncomputable def SubgroupTestValue.SubgroupTestData.valErg (T : SubgroupTestData) : ℝ

The ergodic value (I:497): the supremum of the value over the invariant random subgroups.

Equations

• T.valErg = ⨆ μ ∈ SubgroupTestValue.IRS T.nGen, T.valOn μ

theorem SubgroupTestValue.SubgroupTestData.le_valErg (T : SubgroupTestData) {μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace T.nGen)} (hμ : μ ∈ IRS T.nGen) : T.valOn μ ≤ T.valErg

theorem SubgroupTestValue.SubgroupTestData.valErg_le (T : SubgroupTestData) {a : ℝ} (h : ∀ μ ∈ IRS T.nGen, T.valOn μ ≤ a) (ha : 0 ≤ a) : T.valErg ≤ a

theorem SubgroupTestValue.SubgroupTestData.valErg_le_one (T : SubgroupTestData) : T.valErg ≤ 1

theorem SubgroupTestValue.SubgroupTestData.bddAbove_value (T : SubgroupTestData) : BddAbove (Set.range T.value)

theorem SubgroupTestValue.SubgroupTestData.le_valSof (T : SubgroupTestData) (σ : FiniteAction T.nGen) : T.value σ ≤ T.valSof

theorem SubgroupTestValue.SubgroupTestData.valSof_nonneg (T : SubgroupTestData) : 0 ≤ T.valSof

theorem SubgroupTestValue.SubgroupTestData.valSof_le_one (T : SubgroupTestData) : T.valSof ≤ 1

theorem SubgroupTestValue.SubgroupTestData.valErg_nonneg (T : SubgroupTestData) : 0 ≤ T.valErg

theorem SubgroupTestValue.SubgroupTestData.valSof_le_valErg (T : SubgroupTestData) : T.valSof ≤ T.valErg

The sofic value is at most the ergodic value (I:524).

theorem SubgroupTestValue.SubgroupTestData.valOn_le_valSof_of_mem_closure (T : SubgroupTestData) {μ : MeasureTheory.ProbabilityMeasure (SubgroupSpace T.nGen)} (hμ : μ ∈ closure (finDescIRS T.nGen)) : T.valOn μ ≤ T.valSof

The value of every IRS in the closure of the finitely described ones is at most the sofic value.

theorem SubgroupTestValue.SubgroupTestData.valSof_eq_valErg (T : SubgroupTestData) (hAL : AldousLyons) : T.valSof = T.valErg

Corollary I:550: under the Aldous–Lyons conjecture the sofic and ergodic values of every test are equal.