Subgroup tests, their sofic value, and the Aldous–Lyons conjecture (paper I)

A self-contained statement file, depending on Mathlib only, for The Aldous–Lyons Conjecture I: Subgroup Tests (L. Bowen, M. Chapman, A. Lubotzky, T. Vidick, arXiv:2408.00110, "paper I"; line numbers I:n of its LaTeX source). Its definitions, with the paper's:

• SubgroupTestData (I:439–457): a first-order description of a subgroup test over the free group on nGen generators — finitely many challenges, each a weight, a finite list K of words, and a decision on the subsets of K, given in disjunctive normal form over the literals "the i-th word of K lies (or does not lie) in the subgroup". Every decision function on the subsets of a finite K has such a form; the paper's decisions are arbitrary.
• FiniteAction, SubgroupTestData.value, SubgroupTestData.valSof (I:501–520): a finite action σ of the free group, the value of the finitely described IRS Φ(σ) (the stabilizer of a uniform point) against the test, and the sofic value, its supremum over finite actions.
• SofValueApproximable: the sofic value is computable, in the sense that a computable function approximates it to within 1/(k+1) on every test, on the grid of step 1/(k+1). Paper I deduces the negation of the Aldous–Lyons conjecture from its failure (Corollary I:605 with Main Theorem I, I:594).
• SubgroupSpace, IRS, finDescIRS, AldousLyons (I:467–530): the space of subgroups of the free group as a closed subspace of {0,1}^F with the product topology, the invariant random subgroups, the finitely described ones Φ(σ), and the conjecture that the latter are weak-* dense in the former.

Words are lists of letters (i, e), the generator i (to the power -1 when e), read as a product from left to right; a letter whose generator is not among the nGen acts as the identity. A literal (i, b) with i beyond the length of K is false.

Descriptions of subgroup tests

@[reducible, inline]

abbrev SubgroupTestValue.Letter : Type

A letter: a generator and whether it is inverted.

Equations

• SubgroupTestValue.Letter = (ℕ × Bool)

@[reducible, inline]

abbrev SubgroupTestValue.Word : Type

A word in the generators and their inverses.

Equations

• SubgroupTestValue.Word = List SubgroupTestValue.Letter

structure SubgroupTestValue.SubgroupTestData : Type

A first-order description of a subgroup test (I:439–457) over the free group on nGen generators: a list of challenges (weight, K, clauses). The challenge is passed by a subgroup H when some clause holds, a clause being a list of literals (i, b), each saying that the i-th word of K lies in H when b and does not when ¬b. The challenge distribution is proportional to the weights.

• nGen : ℕ
• challenges : List (ℕ × List Word × List (List (ℕ × Bool)))

def SubgroupTestValue.SubgroupTestData.equivTuple : SubgroupTestData ≃ ℕ × List (ℕ × List Word × List (List (ℕ × Bool)))

SubgroupTestData is a tuple of naturals and lists.

Equations

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

@[instance_reducible]

instance SubgroupTestValue.SubgroupTestData.instPrimcodable : Primcodable SubgroupTestData

Equations

• SubgroupTestValue.SubgroupTestData.instPrimcodable = Primcodable.ofEquiv (ℕ × List (ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool)))) SubgroupTestValue.SubgroupTestData.equivTuple

Finite actions and the value

structure SubgroupTestValue.FiniteAction (nGen : ℕ) : Type

A finite action of the free group on nGen generators: a permutation of Fin N, N ≥ 1, for each generator.

• N : ℕ
• N_pos : 0 < self.N
• σ : Fin nGen → Equiv.Perm (Fin self.N)

def SubgroupTestValue.FiniteAction.letterPerm {nGen : ℕ} (σ : FiniteAction nGen) (l : Letter) : Equiv.Perm (Fin σ.N)

The permutation of a letter.

Equations

• σ.letterPerm l = if h : l.1 < nGen then if l.2 = true then (σ.σ ⟨l.1, h⟩)⁻¹ else σ.σ ⟨l.1, h⟩ else 1

def SubgroupTestValue.FiniteAction.wordPerm {nGen : ℕ} (σ : FiniteAction nGen) (w : Word) : Equiv.Perm (Fin σ.N)

The permutation of a word, the product of its letters from left to right.

Equations

• σ.wordPerm w = (List.map σ.letterPerm w).prod

def SubgroupTestValue.FiniteAction.InStab {nGen : ℕ} (σ : FiniteAction nGen) (x : Fin σ.N) (w : Word) : Prop

The word w lies in the stabilizer Stab(σ, x) of the point x.

Equations

• σ.InStab x w = ((σ.wordPerm w) x = x)

@[instance_reducible]

instance SubgroupTestValue.FiniteAction.instDecidableInStab {nGen : ℕ} (σ : FiniteAction nGen) (x : Fin σ.N) (w : Word) : Decidable (σ.InStab x w)

Equations

• σ.instDecidableInStab x w = id inferInstance

def SubgroupTestValue.FiniteAction.LitHolds {nGen : ℕ} (σ : FiniteAction nGen) (K : List Word) (x : Fin σ.N) (lit : ℕ × Bool) : Prop

The literal (i, b) holds at x for the list of words K.

Equations

• σ.LitHolds K x lit = ∃ (h : lit.1 < K.length), decide (σ.InStab x K[lit.1]) = lit.2

@[instance_reducible]

instance SubgroupTestValue.FiniteAction.instDecidableLitHolds {nGen : ℕ} (σ : FiniteAction nGen) (K : List Word) (x : Fin σ.N) (lit : ℕ × Bool) : Decidable (σ.LitHolds K x lit)

Equations

• σ.instDecidableLitHolds K x lit = id inferInstance

def SubgroupTestValue.FiniteAction.Passes {nGen : ℕ} (σ : FiniteAction nGen) (K : List Word) (clauses : List (List (ℕ × Bool))) (x : Fin σ.N) : Prop

The stabilizer of x passes the challenge (K, clauses): some clause holds.

Equations

• σ.Passes K clauses x = ∃ c ∈ clauses, ∀ lit ∈ c, σ.LitHolds K x lit

@[instance_reducible]

instance SubgroupTestValue.FiniteAction.instDecidablePasses {nGen : ℕ} (σ : FiniteAction nGen) (K : List Word) (clauses : List (List (ℕ × Bool))) (x : Fin σ.N) : Decidable (σ.Passes K clauses x)

Equations

• σ.instDecidablePasses K clauses x = id inferInstance

noncomputable def SubgroupTestValue.FiniteAction.passProb {nGen : ℕ} (σ : FiniteAction nGen) (K : List Word) (clauses : List (List (ℕ × Bool))) : ℝ

The probability that the stabilizer of a uniform point passes the challenge.

Equations

• σ.passProb K clauses = ↑{x : Fin σ.N | σ.Passes K clauses x}.card / ↑σ.N

def SubgroupTestValue.SubgroupTestData.totalWeight (T : SubgroupTestData) : ℕ

The total weight of the challenges.

Equations

• T.totalWeight = (List.map (fun (x : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool))) => x.1) T.challenges).sum

noncomputable def SubgroupTestValue.SubgroupTestData.value (T : SubgroupTestData) (σ : FiniteAction T.nGen) : ℝ

The value val(T, Φ(σ)) (I:455) of the finitely described IRS of σ: the probability that the stabilizer of a uniform point passes a challenge drawn with probability proportional to its weight.

Equations

• T.value σ = (List.map (fun (c : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool))) => ↑c.1 * σ.passProb c.2.1 c.2.2) T.challenges).sum / ↑T.totalWeight

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

The sofic value (I:518): the supremum of the value over finite actions.

Equations

• T.valSof = ⨆ (σ : SubgroupTestValue.FiniteAction T.nGen), T.value σ

def SubgroupTestValue.SofValueApproximable : Prop

The sofic value is approximable: a computable function approximates it to within 1/(k+1) on every test, by a point f T k / (k+1) of the grid of step 1/(k+1) (the value lies in [0, 1]). Paper I shows this follows from the Aldous–Lyons conjecture (Corollary I:605), and, with paper II, that it is false (Corollary I:2144).

Equations

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

Invariant random subgroups and the conjecture

def SubgroupTestValue.IsSubgroupIndicator {s : ℕ} (A : FreeGroup (Fin s) → Bool) : Prop

The indicator functions of the subgroups of the free group on Fin s.

Equations

• SubgroupTestValue.IsSubgroupIndicator A = (A 1 = true ∧ ∀ (v w : FreeGroup (Fin s)), A v = true → A w = true → A (v * w⁻¹) = true)

def SubgroupTestValue.SubgroupSpace (s : ℕ) : Type

The space Sub(F) of subgroups of the free group on Fin s, as indicator functions, with the subspace topology of the product topology on {0,1}^F (I:469).

Equations

• SubgroupTestValue.SubgroupSpace s = { A : FreeGroup (Fin s) → Bool // SubgroupTestValue.IsSubgroupIndicator A }

@[instance_reducible]

instance SubgroupTestValue.instTopologicalSpaceSubgroupSpace (s : ℕ) : TopologicalSpace (SubgroupSpace s)

Equations

• SubgroupTestValue.instTopologicalSpaceSubgroupSpace s = instTopologicalSpaceSubtype

@[instance_reducible]

instance SubgroupTestValue.instMeasurableSpaceSubgroupSpace (s : ℕ) : MeasurableSpace (SubgroupSpace s)

Equations

• SubgroupTestValue.instMeasurableSpaceSubgroupSpace s = borel (SubgroupTestValue.SubgroupSpace s)

instance SubgroupTestValue.instBorelSpaceSubgroupSpace (s : ℕ) : BorelSpace (SubgroupSpace s)

def SubgroupTestValue.conj {s : ℕ} (w : FreeGroup (Fin s)) (H : SubgroupSpace s) : SubgroupSpace s

Conjugation by w on Sub(F): H ↦ w H w⁻¹.

Equations

• SubgroupTestValue.conj w H = ⟨fun (v : FreeGroup (Fin s)) => ↑H (w⁻¹ * v * w), ⋯⟩

def SubgroupTestValue.IRS (s : ℕ) : Set (MeasureTheory.ProbabilityMeasure (SubgroupSpace s))

The invariant random subgroups (Definition I:486): the probability measures on Sub(F) invariant under conjugation.

Equations

• SubgroupTestValue.IRS s = {μ : MeasureTheory.ProbabilityMeasure (SubgroupTestValue.SubgroupSpace s) | ∀ (w : FreeGroup (Fin s)), MeasureTheory.Measure.map (SubgroupTestValue.conj w) ↑μ = ↑μ}

def SubgroupTestValue.stab {s : ℕ} (σ : FiniteAction s) (x : Fin σ.N) : SubgroupSpace s

The stabilizer Stab(σ, x) (I:503) of a point under a finite action, as an indicator.

Equations

• SubgroupTestValue.stab σ x = ⟨fun (v : FreeGroup (Fin s)) => decide (((FreeGroup.lift σ.σ) v) x = x), ⋯⟩

def SubgroupTestValue.finDescIRS (s : ℕ) : Set (MeasureTheory.ProbabilityMeasure (SubgroupSpace s))

The finitely described IRSs Φ(σ) = E_x 1_{Stab(σ, x)} (I:510–514).

Equations

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

def SubgroupTestValue.AldousLyons : Prop

The Aldous–Lyons conjecture (Conjecture I:528): for every finite rank, the finitely described IRSs of the free group are weak-* dense in its IRSs. Paper I with paper II refutes it (Corollary I:2144).

Equations

• SubgroupTestValue.AldousLyons = ∀ (s : ℕ), SubgroupTestValue.IRS s ⊆ closure (SubgroupTestValue.finDescIRS s)