Foundations for the non-sofic group construction

This file develops the finite-permutation, property-T, Leavitt-algebra, and prefix-action infrastructure used by the construction.

@[reducible, inline]

abbrev SoficGroups.UnitaryRepresentation (G : Type u) (H : Type v) [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type (max u v)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.UnitaryRepresentation G H = (G →* H ≃ₗᵢ[ℂ] H)

structure SoficGroups.KazhdanPair (G : Type u) [Group G] : Type u

Internal interface connecting the split non-sofic proof modules.

• generators : Finset G

  Internal interface connecting the split non-sofic proof modules.

• kazhdanConstant : ℝ

  Internal interface connecting the split non-sofic proof modules.

• positive : 0 < self.kazhdanConstant
• invariant (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation G H) (ξ : H) : ‖ξ‖ = 1 → (∀ g ∈ self.generators, ‖(π g) ξ - ξ‖ < self.kazhdanConstant) → ∃ (η : H), η ≠ 0 ∧ ∀ (g : G), (π g) η = η

class SoficGroups.HasPropertyT (G : Type u) [Group G] : Prop

Internal interface connecting the split non-sofic proof modules.

• exists_kazhdanPair : Nonempty (KazhdanPair G)

theorem SoficGroups.hasPropertyT_of_mulEquiv {G : Type u} {G' : Type w} [Group G] [Group G'] (e : G ≃* G') [HasPropertyT G] : HasPropertyT G'

noncomputable def SoficGroups.normalizedHamming {Y : Type u_1} [Fintype Y] [DecidableEq Y] (p q : Equiv.Perm Y) : ℝ

The proportion of points on which two finite permutations differ.

Equations

• SoficGroups.normalizedHamming p q = ↑(hammingDist (fun (y : Y) => p y) fun (y : Y) => q y) / ↑(Fintype.card Y)

@[simp]

theorem SoficGroups.normalizedHamming_self {Y : Type u_1} [Fintype Y] [DecidableEq Y] (p : Equiv.Perm Y) : normalizedHamming p p = 0

theorem SoficGroups.normalizedHamming_comm {Y : Type u_1} [Fintype Y] [DecidableEq Y] (p q : Equiv.Perm Y) : normalizedHamming p q = normalizedHamming q p

theorem SoficGroups.normalizedHamming_nonneg {Y : Type u_1} [Fintype Y] [DecidableEq Y] (p q : Equiv.Perm Y) : 0 ≤ normalizedHamming p q

theorem SoficGroups.normalizedHamming_triangle {Y : Type u_1} [Fintype Y] [DecidableEq Y] (p q r : Equiv.Perm Y) : normalizedHamming p r ≤ normalizedHamming p q + normalizedHamming q r

theorem SoficGroups.normalizedHamming_mul_left {Y : Type u_1} [Fintype Y] [DecidableEq Y] (s p q : Equiv.Perm Y) : normalizedHamming (s * p) (s * q) = normalizedHamming p q

theorem SoficGroups.normalizedHamming_mul_right {Y : Type u_1} [Fintype Y] [DecidableEq Y] (s p q : Equiv.Perm Y) : normalizedHamming (p * s) (q * s) = normalizedHamming p q

structure SoficGroups.PermutationModel (G : Type u_1) [Group G] : Type u_1

A finite permutation-valued approximation to a group action.

• size : ℕ

  The cardinality of the finite model.

• size_pos : 0 < self.size

  The model is nonempty.

• action : G → Equiv.Perm (Fin self.size)

  The permutation assigned to each group element.

• map_one : self.action 1 = 1

  The identity is assigned the identity permutation.

structure SoficGroups.GoodOn {G : Type u_1} [Group G] (M : PermutationModel G) (F : Finset G) (ε : ℝ) : Prop

Multiplication and separation hold on a prescribed finite set.

• multiplicative (g : G) : g ∈ F → ∀ h ∈ F, normalizedHamming (M.action (g * h)) (M.action g * M.action h) < ε

  The model is approximately multiplicative on the prescribed set.

• separated (g : G) : g ∈ F → g ≠ 1 → 1 - ε < normalizedHamming (M.action g) 1

  Nonidentity elements in the prescribed set stay far from the identity permutation.

class SoficGroups.Sofic (G : Type u_1) [Group G] : Prop

A group admitting arbitrarily accurate finite permutation models.

• approximation (F : Finset G) (ε : ℝ) : 0 < ε → ε < 1 → ∃ (M : PermutationModel G), GoodOn M F ε

  Every finite set has a permutation model at every error strictly between zero and one.

structure SoficGroups.SoficApproximation (G : Type u_1) [Group G] : Type u_1

Internal interface connecting the split non-sofic proof modules.

• model : ℕ → PermutationModel G

  Internal interface connecting the split non-sofic proof modules.

• multiplicative (g h : G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((self.model n).action (g * h)) ((self.model n).action g * (self.model n).action h)) Filter.atTop (nhds 0)
• separated (g : G) : g ≠ 1 → Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((self.model n).action g) 1) Filter.atTop (nhds 1)

def SoficGroups.pullbackSoficApproximation {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : H →* G) (hf : Function.Injective ⇑f) (A : SoficApproximation G) : SoficApproximation H

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.pullbackSoficApproximation f hf A = { model := fun (n : ℕ) => SoficGroups.pullbackPermutationModel✝ f (A.model n), multiplicative := ⋯, separated := ⋯ }

theorem SoficGroups.exists_soficApproximation_size_tendsto (G : Type u_1) [Group G] [Countable G] [Sofic G] : ∃ (A : SoficApproximation G), Filter.Tendsto (fun (n : ℕ) => (A.model n).size) Filter.atTop Filter.atTop

theorem SoficGroups.sofic_of_injective {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Sofic G] (f : H →* G) (hf : Function.Injective ⇑f) : Sofic H

theorem SoficGroups.exists_finitelyPresented_not_sofic_of_not_sofic {G : Type u} [Group G] (hG : ¬Sofic G) : ∃ (H : Type u) (x : Group H), Group.IsFinitelyPresented H ∧ ¬Sofic H

structure SoficGroups.LocalMultiplicativeOn {G : Type u} {H : Type v} [Group G] [Group H] (s : Finset G) (f : G → H) : Prop

Internal interface connecting the split non-sofic proof modules.

• map_one : f 1 = 1
• map_mul (x : G) : x ∈ s → ∀ y ∈ s, f (x * y) = f x * f y

class SoficGroups.LEF (G : Type u) [Group G] : Prop

Internal interface connecting the split non-sofic proof modules.

• approximate (s : Finset G) : ∃ (n : ℕ) (f : G → Equiv.Perm (Fin n)), Set.InjOn f ↑s ∧ LocalMultiplicativeOn s f

theorem SoficGroups.LocalMultiplicativeOn.mono {G : Type u} {H : Type v} [Group G] [Group H] {s t : Finset G} {f : G → H} (h : LocalMultiplicativeOn t f) (hst : s ⊆ t) : LocalMultiplicativeOn s f

theorem SoficGroups.exists_local_word_control {α : Type u} {G : Type v} [Group G] (φ : FreeGroup α →* G) (z : FreeGroup α) : ∃ (s : Finset G), ∀ (H : Type w) [inst : Group H] (f : G → H), LocalMultiplicativeOn s f → (FreeGroup.lift fun (a : α) => f (φ (FreeGroup.of a))) z = f (φ z)

def SoficGroups.boundary {V : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (A : Finset V) : ℕ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.boundary σ A = ∑ i : ι, {x ∈ A | (σ i) x ∉ A}.card

def SoficGroups.agreementSet {V : Type u_1} [Fintype V] [DecidableEq V] (c c' : Equiv.Perm V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.agreementSet c c' = {x : V | c x = c' x}

def SoficGroups.permutationCommutationDefect {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (c : Equiv.Perm V) : ℕ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.permutationCommutationDefect σ c = ∑ i : ι, {x : V | c ((σ i) x) ≠ (σ i) (c x)}.card

theorem SoficGroups.agreementSet_card_add_hammingDist {V : Type u_1} [Fintype V] [DecidableEq V] (c c' : Equiv.Perm V) : ((agreementSet c c').card + hammingDist (fun (x : V) => c x) fun (x : V) => c' x) = Fintype.card V

def SoficGroups.inducedBoundary {V : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (B E : Finset V) : ℕ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.inducedBoundary σ B E = ∑ i : ι, {x ∈ E | (σ i) x ∉ B ∧ (σ i) x ∉ E}.card

theorem SoficGroups.exists_pruned_expander {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (γ ell a : ℝ) (hgap : ell < γ) (hadd : ∀ (A : Finset V), γ * min (↑A.card) (↑(Fintype.card V) - ↑A.card) - a * ↑(Fintype.card V) ≤ ↑(boundary σ A)) (hsmall : 2 * a * (2 * (γ - ell) + ↑(Fintype.card ι)) ≤ (γ - ell) ^ 2) : ∃ (B : Finset V), 2 * B.card ≤ Fintype.card V ∧ ↑B.card ≤ a * ↑(Fintype.card V) / (γ - ell) ∧ ∀ (E : Finset V), Disjoint B E → 2 * E.card ≤ Fintype.card V - B.card → ell * ↑E.card ≤ ↑(inducedBoundary σ B E)

def SoficGroups.matchedRetainedSupport {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.matchedRetainedSupport R = R.biUnion id

def SoficGroups.matchedCore {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) (D : Finset V → Finset V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.matchedCore R D = R.biUnion fun (C : Finset V) => C ∩ D C

def SoficGroups.partitionWordCrossing {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (w : Equiv.Perm V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.partitionWordCrossing P w = {x ∈ U | w x ∉ P.part x}

def SoficGroups.matchedWordPreimageBad {V : Type u_1} [DecidableEq V] (U : Finset V) (R : Finset (Finset V)) (D : Finset V → Finset V) (w : Equiv.Perm V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.matchedWordPreimageBad U R D w = {x ∈ U | w x ∈ U \ SoficGroups.matchedCore R D}

theorem SoficGroups.finpartition_dominant_matching_injOn {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (R : Finset (Finset V)) (hR : R ⊆ P.parts) (D : Finset V → Finset V) (hmajor : ∀ C ∈ R, (D C).card < 2 * (C ∩ D C).card) : Set.InjOn D ↑R

theorem SoficGroups.matchedRetainedSupport_subset {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (R : Finset (Finset V)) (hR : R ⊆ P.parts) : matchedRetainedSupport R ⊆ U

theorem SoficGroups.matchedRetainedSupport_card {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (R : Finset (Finset V)) (hR : R ⊆ P.parts) : (matchedRetainedSupport R).card = ∑ C ∈ R, C.card

theorem SoficGroups.matchedCore_missing_card {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (R : Finset (Finset V)) (hR : R ⊆ P.parts) (D : Finset V → Finset V) : (U \ matchedCore R D).card = (U \ matchedRetainedSupport R).card + ∑ C ∈ R, (C \ D C).card

theorem SoficGroups.matchedWordPreimageBad_card_le {V : Type u_1} [DecidableEq V] (U : Finset V) (R : Finset (Finset V)) (D : Finset V → Finset V) (w : Equiv.Perm V) : (matchedWordPreimageBad U R D w).card ≤ (U \ matchedCore R D).card

theorem SoficGroups.exists_completion_of_internal_permutation {V : Type u_1} [Finite V] (p : Equiv.Perm V) (Z : Finset V) : ∃ (q : Equiv.Perm ↥Z), ∀ (x : V) (hx : x ∈ Z), p x ∈ Z → ↑(q ⟨x, hx⟩) = p x

theorem SoficGroups.exists_diverging_radius_with_vanishing_diagonal_error (e : ℕ → ℕ → ℝ) (hnonneg : ∀ (n k : ℕ), 0 ≤ e n k) (he : ∀ (k : ℕ), Filter.Tendsto (fun (n : ℕ) => e n k) Filter.atTop (nhds 0)) : ∃ (r : ℕ → ℕ), Filter.Tendsto r Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => e n (r n)) Filter.atTop (nhds 0)

theorem SoficGroups.finite_union_bad_density_tendsto_zero {α : ℕ → Type u_1} [(n : ℕ) → DecidableEq (α n)] {ι : Type u_2} (I : Finset ι) (V : (n : ℕ) → Finset (α n)) (B : (n : ℕ) → ι → Finset (α n)) (hbad : ∀ i ∈ I, Filter.Tendsto (fun (n : ℕ) => ↑(V n ∩ B n i).card / ↑(V n).card) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(V n ∩ I.biUnion (B n)).card / ↑(V n).card) Filter.atTop (nhds 0)

theorem SoficGroups.sum_card_inter_partition {α : Type u_1} [DecidableEq α] {U : Finset α} (P : Finpartition U) (B : Finset α) : ∑ C ∈ P.parts, (C ∩ B).card = (U ∩ B).card

theorem SoficGroups.retained_bad_density_tendsto_zero {α : ℕ → Type u_1} [(n : ℕ) → DecidableEq (α n)] (V U B : (n : ℕ) → Finset (α n)) (hV : ∀ (n : ℕ), (V n).Nonempty) (hU : ∀ (n : ℕ), (U n).Nonempty) (hUV : ∀ (n : ℕ), U n ⊆ V n) (hcover : Filter.Tendsto (fun (n : ℕ) => ↑(U n).card / ↑(V n).card) Filter.atTop (nhds 1)) (hbad : Filter.Tendsto (fun (n : ℕ) => ↑(V n ∩ B n).card / ↑(V n).card) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(U n ∩ B n).card / ↑(U n).card) Filter.atTop (nhds 0)

inductive SoficGroups.LeavittGenerator : Type

Internal interface connecting the split non-sofic proof modules.

• s : Fin 2 → LeavittGenerator
• t : Fin 2 → LeavittGenerator

@[instance_reducible]

instance SoficGroups.instFintypeLeavittGenerator : Fintype LeavittGenerator

Equations

• SoficGroups.instFintypeLeavittGenerator = Fintype.ofEquiv (Fin 2 ⊕ Fin 2) SoficGroups.LeavittGenerator.proxyTypeEquiv

@[reducible, inline]

abbrev SoficGroups.LeavittFree : Type

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.LeavittFree = FreeAlgebra (ZMod 2) SoficGroups.LeavittGenerator

inductive SoficGroups.LeavittRelation : LeavittFree → LeavittFree → Prop

Internal interface connecting the split non-sofic proof modules.

• inverse (i j : Fin 2) : LeavittRelation (FreeAlgebra.ι (ZMod 2) (LeavittGenerator.t i) * FreeAlgebra.ι (ZMod 2) (LeavittGenerator.s j)) (if i = j then 1 else 0)
• partition : LeavittRelation (FreeAlgebra.ι (ZMod 2) (LeavittGenerator.s 0) * FreeAlgebra.ι (ZMod 2) (LeavittGenerator.t 0) + FreeAlgebra.ι (ZMod 2) (LeavittGenerator.s 1) * FreeAlgebra.ι (ZMod 2) (LeavittGenerator.t 1)) 1

@[reducible, inline]

abbrev SoficGroups.BinaryLeavitt : Type

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.BinaryLeavitt = RingQuot SoficGroups.LeavittRelation

instance SoficGroups.binaryLeavittFiniteType : Algebra.FiniteType (ZMod 2) BinaryLeavitt

instance SoficGroups.binaryLeavittNontrivial : Nontrivial BinaryLeavitt

def SoficGroups.leavittWordS : List (Fin 2) → BinaryLeavitt

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.leavittWordS [] = 1
• SoficGroups.leavittWordS (i :: a) = SoficGroups.leavittS✝ i * SoficGroups.leavittWordS a

def SoficGroups.leavittWordT : List (Fin 2) → BinaryLeavitt

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.leavittWordT [] = 1
• SoficGroups.leavittWordT (i :: a) = SoficGroups.leavittWordT a * SoficGroups.leavittT✝ i

theorem SoficGroups.leavittWordT_mul_wordS_self (a : List (Fin 2)) : leavittWordT a * leavittWordS a = 1

theorem SoficGroups.leavittWordT_mul_wordS_of_incomparable (a b : List (Fin 2)) (hab : ¬a <+: b) (hba : ¬b <+: a) : leavittWordT a * leavittWordS b = 0

theorem SoficGroups.leavittWordS_append (a b : List (Fin 2)) : leavittWordS (a ++ b) = leavittWordS a * leavittWordS b

theorem SoficGroups.leavittWordT_append (a b : List (Fin 2)) : leavittWordT (a ++ b) = leavittWordT b * leavittWordT a

def SoficGroups.leavittCylinder (a : List (Fin 2)) : BinaryLeavitt

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.leavittCylinder a = SoficGroups.leavittWordS a * SoficGroups.leavittWordT a

structure SoficGroups.BinaryPrefixCode (ι : Type u_1) : Type u_1

Internal interface connecting the split non-sofic proof modules.

• word : ι → List (Fin 2)

  Internal interface connecting the split non-sofic proof modules.

• prefix_free ⦃i j : ι⦄ : i ≠ j → ¬self.word i <+: self.word j

def SoficGroups.alphaPrefixCode : BinaryPrefixCode (Fin 3)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.alphaPrefixCode = { word := SoficGroups.alphaWord✝, prefix_free := SoficGroups.alphaPrefixCode._proof_1✝ }

def SoficGroups.ninePrefixCode : BinaryPrefixCode (Fin 9)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.ninePrefixCode = { word := SoficGroups.nineWord✝, prefix_free := SoficGroups.ninePrefixCode._proof_1✝ }

def SoficGroups.compressionU : BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.compressionU = SoficGroups.prefixTableUnit✝ SoficGroups.ninePrefixCode SoficGroups.uPrefixCode✝ SoficGroups.ninePrefixCode_complete✝ SoficGroups.uPrefixCode_complete✝

def SoficGroups.compressionV : BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.compressionV = SoficGroups.prefixTableUnit✝ SoficGroups.ninePrefixCode SoficGroups.vPrefixCode✝ SoficGroups.ninePrefixCode_complete✝ SoficGroups.vPrefixCode_complete✝

def SoficGroups.alphaZeroPrefixCode : BinaryPrefixCode (Fin 3)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.alphaZeroPrefixCode = { word := fun (i : Fin 3) => SoficGroups.alphaWord✝ i ++ [0], prefix_free := SoficGroups.alphaZeroPrefixCode._proof_1✝ }

def SoficGroups.prefixElementaryGroup {ι : Type u_1} [DecidableEq ι] (E : BinaryPrefixCode ι) : Subgroup BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.compressionU_map_alphaPrefixElementaryGroup : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj compressionU)) (prefixElementaryGroup alphaPrefixCode) = prefixElementaryGroup alphaZeroPrefixCode

theorem SoficGroups.compressionV_map_alphaPrefixElementaryGroup : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj compressionV)) (prefixElementaryGroup alphaPrefixCode) = prefixElementaryGroup alphaZeroPrefixCode

theorem SoficGroups.alphaZero_prefixElementaryGroup_le : prefixElementaryGroup alphaZeroPrefixCode ≤ prefixElementaryGroup alphaPrefixCode

def SoficGroups.elementaryUnit {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Ring R] (i j : ι) (h : i ≠ j) (a : R) : (Matrix ι ι R)ˣ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.elementaryUnit i j h a = { val := 1 + Matrix.single i j a, inv := 1 - Matrix.single i j a, val_inv := ⋯, inv_val := ⋯ }

def SoficGroups.elementaryGroup (ι : Type u_3) (R : Type u_4) [Fintype ι] [DecidableEq ι] [Ring R] : Subgroup (Matrix ι ι R)ˣ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.elementaryGroup ι R = Subgroup.closure {z : (Matrix ι ι R)ˣ | ∃ (i : ι) (j : ι) (h : i ≠ j) (a : R), SoficGroups.elementaryUnit i j h a = z}

theorem SoficGroups.elementaryUnit_mem {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Ring R] (i j : ι) (h : i ≠ j) (a : R) : elementaryUnit i j h a ∈ elementaryGroup ι R

def SoficGroups.elementaryRootHom {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Ring R] (i j : ι) (h : i ≠ j) : Multiplicative R →* ↥(elementaryGroup ι R)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.elementaryRootHom i j h = { toFun := fun (a : Multiplicative R) => ⟨SoficGroups.elementaryUnit i j h (Multiplicative.toAdd a), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem SoficGroups.elementaryUnit_commutator {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Ring R] (i j k : ι) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a b : R) : ⁅elementaryUnit i j hij a, elementaryUnit j k hjk b⁆ = elementaryUnit i k hik (a * b)

theorem SoficGroups.elementaryUnit_mem_of_two_step {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Ring R] (H : Subgroup (Matrix ι ι R)ˣ) (i j k : ι) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a : R) (hleft : elementaryUnit i j hij a ∈ H) (hright : elementaryUnit j k hjk 1 ∈ H) : elementaryUnit i k hik a ∈ H

def SoficGroups.elementaryCoefficientSubalgebra {R : Type u_1} [Ring R] [Algebra (ZMod 2) R] (n : ℕ) (hn : 2 < n) (H : Subgroup (Matrix (Fin n) (Fin n) R)ˣ) (hunit : ∀ (i j : Fin n) (h : i ≠ j), elementaryUnit i j h 1 ∈ H) : Subalgebra (ZMod 2) R

Internal interface connecting the split non-sofic proof modules.

Equations

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

@[reducible, inline]

abbrev SoficGroups.binaryLeavittElementaryGroup (n : ℕ) : Type

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.binaryLeavittElementaryGroup n = ↥(SoficGroups.elementaryGroup (Fin n) SoficGroups.BinaryLeavitt)

def SoficGroups.ninePrefixElementaryGroupEquiv : binaryLeavittElementaryGroup 9 ≃* ↥(prefixElementaryGroup ninePrefixCode)

Internal interface connecting the split non-sofic proof modules.

Equations

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

def SoficGroups.SourceGeneration.sourceGeneratedGroup : Subgroup BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.SourceGeneration.alphaPrefixElementaryGroup_le_nine : prefixElementaryGroup alphaPrefixCode ≤ prefixElementaryGroup ninePrefixCode

theorem SoficGroups.binaryLeavittEL3_infinite : Infinite (binaryLeavittElementaryGroup 3)

theorem SoficGroups.alphaPrefixElementaryGroup_finitelyGenerated : Group.FG ↥(prefixElementaryGroup alphaPrefixCode)

theorem SoficGroups.ninePrefixElementaryGroup_countable : Countable ↥(prefixElementaryGroup ninePrefixCode)

noncomputable def SoficGroups.midrankVariance (ps : List ℝ) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.midrankVariance ps = SoficGroups.midrankSecondMoment✝ 0 ps - SoficGroups.midrankFirstMoment✝ 0 ps ^ 2

noncomputable def SoficGroups.componentRankMass {V : Type u_1} (C : Finset V) (b : V → ℤ) (j : ℤ) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.componentRankMass C b j = ↑{x ∈ C | b x = j}.card / ↑C.card

noncomputable def SoficGroups.componentVertexMidrank {V : Type u_1} (C : Finset V) (b : V → ℤ) (x : V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.componentVertexMidrank C b x = (↑{z ∈ C | b z < b x}.card + ↑{z ∈ C | b z = b x}.card / 2) / ↑C.card

theorem SoficGroups.componentVertexMidrank_nonneg {V : Type u_1} (C : Finset V) (b : V → ℤ) (x : V) : 0 ≤ componentVertexMidrank C b x

theorem SoficGroups.componentVertexMidrank_le_one {V : Type u_1} (C : Finset V) (b : V → ℤ) (x : V) : componentVertexMidrank C b x ≤ 1

noncomputable def SoficGroups.componentRankMassList {V : Type u_1} (C : Finset V) (b : V → ℤ) : List ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.componentRankMassList C b = List.map (SoficGroups.componentRankMass C b) ((Finset.image b C).sort fun (x1 x2 : ℤ) => x1 ≤ x2)

theorem SoficGroups.exists_maximal_componentRankMass {V : Type u_1} (C : Finset V) (b : V → ℤ) (hC : C.Nonempty) : ∃ j ∈ Finset.image b C, ∀ k ∈ Finset.image b C, componentRankMass C b k ≤ componentRankMass C b j

theorem SoficGroups.actual_weighted_midrank_dominant_mass_le {V : Type u_1} {ι : Type u_2} (I : Finset ι) (C : ι → Finset V) (b : V → ℤ) (j : ι → ℤ) (hC : ∀ i ∈ I, (C i).Nonempty) (hmax : ∀ i ∈ I, ∀ k ∈ Finset.image b (C i), componentRankMass (C i) b k ≤ componentRankMass (C i) b (j i)) : ∑ i ∈ I, ↑((C i).card - {x ∈ C i | b x = j i}.card) ≤ 12 * ∑ i ∈ I, ↑(C i).card * midrankVariance (componentRankMassList (C i) b)

theorem SoficGroups.sum_card_component_inter_partition {V : Type u} [DecidableEq V] {U : Finset V} (Q : Finpartition U) (C : Finset V) (hCU : C ⊆ U) : ∑ D ∈ Q.parts, (C ∩ D).card = C.card

noncomputable def SoficGroups.maximumOverlapPart {V : Type u} [DecidableEq V] {U : Finset V} (Q : Finpartition U) (C : Finset V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.maximumOverlapPart Q C = if h : C.Nonempty ∧ C ⊆ U then ⋯.choose else ∅

theorem SoficGroups.maximumOverlapPart_mem {V : Type u} [DecidableEq V] {U : Finset V} (Q : Finpartition U) (C : Finset V) (hC : C.Nonempty) (hCU : C ⊆ U) : maximumOverlapPart Q C ∈ Q.parts

theorem SoficGroups.maximumOverlapPart_maximal {V : Type u} [DecidableEq V] {U : Finset V} (Q : Finpartition U) (C : Finset V) (hC : C.Nonempty) (hCU : C ⊆ U) (E : Finset V) : E ∈ Q.parts → (C ∩ E).card ≤ (C ∩ maximumOverlapPart Q C).card

theorem SoficGroups.compressionU_mem_ninePrefixElementaryGroup : compressionU ∈ prefixElementaryGroup ninePrefixCode

theorem SoficGroups.compressionV_mem_ninePrefixElementaryGroup : compressionV ∈ prefixElementaryGroup ninePrefixCode

theorem SoficGroups.sourceGeneratedGroup_eq_nine : SourceGeneration.sourceGeneratedGroup = prefixElementaryGroup ninePrefixCode

noncomputable def SoficGroups.rankDropCount {ι : Type u_1} [Fintype ι] (u v : ι → ℝ) (H r : ℝ) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.rankDropCount u v H r = ∑ i : ι, if ⌊(v i + r) / H⌋ < ⌊(u i + r) / H⌋ then 1 else 0

noncomputable def SoficGroups.CheegerPoincare.positiveSupport {V : Type u_1} [Fintype V] (f : V → ℝ) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CheegerPoincare.positiveSupport f = {x : V | 0 < f x}

@[simp]

theorem SoficGroups.CheegerPoincare.mem_positiveSupport {V : Type u_1} [Fintype V] (f : V → ℝ) (x : V) : x ∈ positiveSupport f ↔ 0 < f x

noncomputable def SoficGroups.CheegerPoincare.finiteMean {V : Type u_1} [Fintype V] (f : V → ℝ) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CheegerPoincare.finiteMean f = (∑ x : V, f x) / ↑(Fintype.card V)

theorem SoficGroups.CheegerPoincare.sum_sq_sub_finiteMean_le {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) (c : ℝ) : ∑ x : V, (f x - finiteMean f) ^ 2 ≤ ∑ x : V, (f x - c) ^ 2

noncomputable def SoficGroups.CheegerPoincare.lowerLevel {V : Type u_1} [Fintype V] (f : V → ℝ) (a : ℝ) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CheegerPoincare.lowerLevel f a = {x : V | f x < a}

noncomputable def SoficGroups.CheegerPoincare.upperLevel {V : Type u_1} [Fintype V] (f : V → ℝ) (a : ℝ) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CheegerPoincare.upperLevel f a = {x : V | a < f x}

@[simp]

theorem SoficGroups.CheegerPoincare.mem_lowerLevel {V : Type u_1} [Fintype V] (f : V → ℝ) (a : ℝ) (x : V) : x ∈ lowerLevel f a ↔ f x < a

@[simp]

theorem SoficGroups.CheegerPoincare.mem_upperLevel {V : Type u_1} [Fintype V] (f : V → ℝ) (a : ℝ) (x : V) : x ∈ upperLevel f a ↔ a < f x

theorem SoficGroups.CheegerPoincare.exists_finite_real_median {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : ∃ (m : ℝ), 2 * (lowerLevel f m).card ≤ Fintype.card V ∧ 2 * (upperLevel f m).card ≤ Fintype.card V

theorem SoficGroups.CheegerPoincare.positiveSupport_max_sub {V : Type u_1} [Fintype V] (f : V → ℝ) (m : ℝ) : (positiveSupport fun (x : V) => max (f x - m) 0) = upperLevel f m

theorem SoficGroups.CheegerPoincare.positiveSupport_max_sub_reverse {V : Type u_1} [Fintype V] (f : V → ℝ) (m : ℝ) : (positiveSupport fun (x : V) => max (m - f x) 0) = lowerLevel f m

noncomputable def SoficGroups.CheegerPoincare.finiteVariance {V : Type u_1} [Fintype V] (f : V → ℝ) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CheegerPoincare.finiteVariance f = (∑ x : V, (f x - SoficGroups.CheegerPoincare.finiteMean f) ^ 2) / ↑(Fintype.card V)

theorem SoficGroups.CheegerPoincare.finiteVariance_nonneg {V : Type u_1} [Fintype V] (f : V → ℝ) : 0 ≤ finiteVariance f

theorem SoficGroups.CheegerPoincare.card_mul_finiteVariance {V : Type u_1} [Fintype V] [Nonempty V] (f : V → ℝ) : ↑(Fintype.card V) * finiteVariance f = ∑ x : V, (f x - finiteMean f) ^ 2

theorem SoficGroups.target_majority_of_small_symmDiff {V : Type u_1} [DecidableEq V] (C D : Finset V) (hsmall : 2 * (symmDiff C D).card < C.card) : D.card < 2 * (C ∩ D).card

def SoficGroups.matchedRetainedFinpartition {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (R : Finset (Finset V)) (hR : R ⊆ P.parts) : Finpartition (matchedRetainedSupport R)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.matchedRetainedFinpartition P R hR = P.ofSubset hR ⋯

theorem SoficGroups.matchedRetainedSupport_nonempty {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (R : Finset (Finset V)) (hR : R ⊆ P.parts) (hRne : R.Nonempty) : (matchedRetainedSupport R).Nonempty

theorem SoficGroups.matchedRetainedSupport_cover_density_tendsto_one {V : ℕ → Type u_1} [(n : ℕ) → DecidableEq (V n)] (U : (n : ℕ) → Finset (V n)) (hU : ∀ (n : ℕ), (U n).Nonempty) (P : (n : ℕ) → Finpartition (U n)) (R : (n : ℕ) → Finset (Finset (V n))) (hR : ∀ (n : ℕ), R n ⊆ (P n).parts) (hdiscard : Filter.Tendsto (fun (n : ℕ) => ↑(U n \ matchedRetainedSupport (R n)).card / ↑(U n).card) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(matchedRetainedSupport (R n)).card / ↑(U n).card) Filter.atTop (nhds 1)

theorem SoficGroups.exists_matched_slow_diagonal_word_errors {V : ℕ → Type u_1} [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} (U : (n : ℕ) → Finset (V n)) (P Q : (n : ℕ) → Finpartition (U n)) (R : (n : ℕ) → Finset (Finset (V n))) (hR : ∀ (n : ℕ), R n ⊆ (P n).parts) (D : (n : ℕ) → Finset (V n) → Finset (V n)) (hD : ∀ (n : ℕ), ∀ C ∈ R n, D n C ∈ (Q n).parts) (hmajor : ∀ (n : ℕ), ∀ C ∈ R n, (D n C).card < 2 * (C ∩ D n C).card) (hdiscard : Filter.Tendsto (fun (n : ℕ) => ↑(U n \ matchedRetainedSupport (R n)).card / ↑(U n).card) Filter.atTop (nhds 0)) (hsymm : Filter.Tendsto (fun (n : ℕ) => ↑(∑ C ∈ R n, (symmDiff C (D n C)).card) / ↑(U n).card) Filter.atTop (nhds 0)) (I : ℕ → Finset ι) (w : (n : ℕ) → ι → Equiv.Perm (V n)) (hword : ∀ (k : ℕ), Filter.Tendsto (fun (n : ℕ) => ↑(∑ i ∈ I k, (partitionWordCrossing (Q n) (w n i)).card) / ↑(U n).card) Filter.atTop (nhds 0)) (B : (n : ℕ) → ℕ → Finset (V n)) (hbad : ∀ (k : ℕ), Filter.Tendsto (fun (n : ℕ) => ↑(U n ∩ B n k).card / ↑(U n).card) Filter.atTop (nhds 0)) : ∃ (r : ℕ → ℕ), Filter.Tendsto r Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => (↑(∑ i ∈ I (r n), (partitionWordCrossing (P n) (w n i)).card) + ↑(U n ∩ B n (r n)).card) / ↑(U n).card) Filter.atTop (nhds 0)

def SoficGroups.matchedRadiusBad {V : Type u_1} {ι : Type u_2} [DecidableEq V] {U : Finset V} (P : Finpartition U) (I : Finset ι) (w : ι → Equiv.Perm V) (B : Finset V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.matchedRadiusBad P I w B = B ∪ I.biUnion fun (i : ι) => SoficGroups.partitionWordCrossing P (w i)

theorem SoficGroups.matchedRadiusBad_card_le {V : Type u_1} {ι : Type u_2} [DecidableEq V] {U : Finset V} (P : Finpartition U) (I : Finset ι) (w : ι → Equiv.Perm V) (B : Finset V) : (U ∩ matchedRadiusBad P I w B).card ≤ (U ∩ B).card + ∑ i ∈ I, (partitionWordCrossing P (w i)).card

theorem SoficGroups.matched_exists_le_weighted_average {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (weight bad : ι → ℝ) (hweight : ∀ i ∈ s, 0 < weight i) : ∃ i ∈ s, bad i / weight i ≤ (∑ j ∈ s, bad j) / ∑ j ∈ s, weight j

theorem SoficGroups.matched_sum_card_inter_partition {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (B : Finset V) : ∑ C ∈ P.parts, (C ∩ B).card = (U ∩ B).card

theorem SoficGroups.matchedRetained_bad_density_tendsto_zero {V : ℕ → Type u_1} [(n : ℕ) → DecidableEq (V n)] (U : (n : ℕ) → Finset (V n)) (hU : ∀ (n : ℕ), (U n).Nonempty) (P : (n : ℕ) → Finpartition (U n)) (R : (n : ℕ) → Finset (Finset (V n))) (hR : ∀ (n : ℕ), R n ⊆ (P n).parts) (hRne : ∀ (n : ℕ), (R n).Nonempty) (hdiscard : Filter.Tendsto (fun (n : ℕ) => ↑(U n \ matchedRetainedSupport (R n)).card / ↑(U n).card) Filter.atTop (nhds 0)) (B : (n : ℕ) → Finset (V n)) (hbad : Filter.Tendsto (fun (n : ℕ) => ↑(U n ∩ B n).card / ↑(U n).card) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(matchedRetainedSupport (R n) ∩ B n).card / ↑(matchedRetainedSupport (R n)).card) Filter.atTop (nhds 0)

theorem SoficGroups.matched_eventually_exists_good_vertex {V : ℕ → Type u_1} [(n : ℕ) → DecidableEq (V n)] (C B : (n : ℕ) → Finset (V n)) (hC : ∀ (n : ℕ), (C n).Nonempty) (hbad : Filter.Tendsto (fun (n : ℕ) => ↑(C n ∩ B n).card / ↑(C n).card) Filter.atTop (nhds 0)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ x ∈ C n, x ∉ B n

theorem SoficGroups.ComponentMidrankVariance.componentVertexMidrank_finiteVariance_eq {V : Type u_1} (C : Finset V) (b : V → ℤ) (hC : C.Nonempty) : (CheegerPoincare.finiteVariance fun (x : ↥C) => componentVertexMidrank C b ↑x) = midrankVariance (componentRankMassList C b)

noncomputable def SoficGroups.insufficientOverlapComponents {V : Type u} [DecidableEq V] {U : Finset V} (P Q : Finpartition U) (eta : ℝ) : Finset (Finset V)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.insufficientOverlapComponents P Q eta = {C ∈ P.parts | ↑(C ∩ SoficGroups.maximumOverlapPart Q C).card < (1 - eta) * ↑C.card}

theorem SoficGroups.insufficientOverlapComponents_subset {V : Type u} [DecidableEq V] {U : Finset V} (P Q : Finpartition U) (eta : ℝ) : insufficientOverlapComponents P Q eta ⊆ P.parts

theorem SoficGroups.insufficientOverlapComponents_mass_le_loss {V : Type u} [DecidableEq V] {U : Finset V} (P Q : Finpartition U) (eta : ℝ) : eta * ∑ C ∈ insufficientOverlapComponents P Q eta, ↑C.card ≤ ∑ C ∈ P.parts, (↑C.card - ↑(C ∩ maximumOverlapPart Q C).card)

noncomputable def SoficGroups.transportedUnivFinpartition {V : Type u} [Fintype V] [DecidableEq V] (Q : Finpartition Finset.univ) (T : Equiv.Perm V) : Finpartition Finset.univ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.transportedUnivFinpartition Q T = (SoficGroups.transportedFinpartition✝ Q T).copy ⋯

@[simp]

theorem SoficGroups.transportedUnivFinpartition_parts {V : Type u} [Fintype V] [DecidableEq V] (Q : Finpartition Finset.univ) (T : Equiv.Perm V) : (transportedUnivFinpartition Q T).parts = Finset.image (fun (C : Finset V) => Finset.map (Equiv.toEmbedding T) C) Q.parts

noncomputable def SoficGroups.partitionComponentSize {V : Type u} [DecidableEq V] {U : Finset V} (Q : Finpartition U) (x : V) : ℕ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.partitionComponentSize Q x = (Q.part x).card

theorem SoficGroups.partitionComponentSize_eq_card_of_mem {V : Type u} [DecidableEq V] {U : Finset V} (Q : Finpartition U) (C : Finset V) (hC : C ∈ Q.parts) (x : V) (hx : x ∈ C) : partitionComponentSize Q x = C.card

theorem SoficGroups.maximumOverlapPart_overlap_of_not_mem_insufficient {V : Type u} [DecidableEq V] {U : Finset V} (P Q : Finpartition U) (eta : ℝ) (C : Finset V) (hC : C ∈ P.parts) (hretained : C ∉ insufficientOverlapComponents P Q eta) : (1 - eta) * ↑C.card ≤ ↑(C ∩ maximumOverlapPart Q C).card

theorem SoficGroups.partitionComponentSize_transport_lower_of_retained {V : Type u} [Fintype V] [DecidableEq V] (Q : Finpartition Finset.univ) (T : Equiv.Perm V) (C : Finset V) (hC : C ∈ Q.parts) (eta : ℝ) (hretained : Finset.map (Equiv.toEmbedding T) C ∉ insufficientOverlapComponents (transportedUnivFinpartition Q T) Q eta) (x : V) (hx : x ∈ C) (hTx : T x ∈ maximumOverlapPart Q (Finset.map (Equiv.toEmbedding T) C)) : (1 - eta) * ↑(partitionComponentSize Q x) ≤ ↑(partitionComponentSize Q (T x))

def SoficGroups.ThompsonPrefixInsertion.prefixInsertionHom (a : List (Fin 2)) : BinaryLeavittˣ →* BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.ThompsonPrefixInsertion.prefixInsertionHom_injective (a : List (Fin 2)) : Function.Injective ⇑(prefixInsertionHom a)

theorem SoficGroups.ThompsonPrefixInsertion.prefixInsertionHom_val (a : List (Fin 2)) (u : BinaryLeavittˣ) : ↑((prefixInsertionHom a) u) = leavittWordS a * ↑u * leavittWordT a + (1 - leavittCylinder a)

def SoficGroups.ThompsonPrefixInsertion.cylinderSwap (a b : List (Fin 2)) (hab : ¬a <+: b) (hba : ¬b <+: a) : BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

def SoficGroups.ThompsonPrefixInsertion.binaryPrefixTranspositionGroup : Subgroup BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

def SoficGroups.ThompsonPrefixInsertion.localPrefixTranspositionGroup (l : List (Fin 2)) : Subgroup BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.ThompsonPrefixInsertion.sourceLocalPrefixTranspositionGroup_le_alpha_sourceWord : localPrefixTranspositionGroup [0, 0, 0, 1] ≤ prefixElementaryGroup alphaPrefixCode

def SoficGroups.ThompsonPrefixInsertion.sourceCompressedLocalProductHom : ↥(prefixElementaryGroup alphaZeroPrefixCode) × ↥(localPrefixTranspositionGroup [0, 0, 0, 1]) →* BinaryLeavittˣ

Internal interface connecting the split non-sofic proof modules.

Equations

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

def SoficGroups.ThompsonPrefixInsertion.sourceCompressedLocalProductEmbedding : ↥(prefixElementaryGroup alphaZeroPrefixCode) × ↥(localPrefixTranspositionGroup [0, 0, 0, 1]) →* ↥(prefixElementaryGroup ninePrefixCode)

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.ThompsonPrefixInsertion.sourceCompressedLocalProductEmbedding_injective : Function.Injective ⇑sourceCompressedLocalProductEmbedding

noncomputable def SoficGroups.MidrankPermutationEnergy.partitionVertexMidrank {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (b : V → ℤ) (x : V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.MidrankPermutationEnergy.partitionVertexMidrank P b x = SoficGroups.componentVertexMidrank (P.part x) b x

def SoficGroups.MidrankPermutationEnergy.rankDecreasingVertices {V : Type u_1} (U : Finset V) (b : V → ℤ) (p : Equiv.Perm V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.MidrankPermutationEnergy.rankDecreasingVertices U b p = {x ∈ U | b (p x) < b x}

noncomputable def SoficGroups.MidrankPermutationEnergy.offsetFloorRank {V : Type u_1} (u : V → ℝ) (H r : ℝ) : V → ℤ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.MidrankPermutationEnergy.offsetFloorRank u H r x = ⌊(u x + r) / H⌋

theorem SoficGroups.MidrankPermutationEnergy.rankDropCount_eq_sum_rankDecreasingVertices {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] (u : V → ℝ) (p : ι → Equiv.Perm V) (H r : ℝ) : rankDropCount (fun (e : ι × V) => u e.2) (fun (e : ι × V) => u ((p e.1) e.2)) H r = ∑ i : ι, ↑(rankDecreasingVertices Finset.univ (offsetFloorRank u H r) (p i)).card

theorem SoficGroups.MidrankPermutationEnergy.partitionVertexMidrank_permutation_energy_tendsto_zero (V : ℕ → Type u_1) (ι : ℕ → Type u_2) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] [(n : ℕ) → Fintype (ι n)] (P : (n : ℕ) → Finpartition Finset.univ) (b : (n : ℕ) → V n → ℤ) (p : (n : ℕ) → ι n → Equiv.Perm (V n)) (N : ℕ → ℝ) (hN : ∀ (n : ℕ), 0 < N n) (hcross : Filter.Tendsto (fun (n : ℕ) => (∑ i : ι n, ↑(partitionWordCrossing (P n) (p n i)).card) / N n) Filter.atTop (nhds 0)) (hrank : Filter.Tendsto (fun (n : ℕ) => (∑ i : ι n, ↑(rankDecreasingVertices Finset.univ (b n) (p n i)).card) / N n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (∑ i : ι n, ∑ x : V n, (partitionVertexMidrank (P n) (b n) ((p n i) x) - partitionVertexMidrank (P n) (b n) x) ^ 2) / N n) Filter.atTop (nhds 0)

def SoficGroups.RankArcCharging.selectedRankSupport {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (b : V → ℤ) (j : Finset V → ℤ) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.RankArcCharging.selectedRankSupport P b j = P.parts.biUnion fun (C : Finset V) => {x ∈ C | b x = j C}

def SoficGroups.RankArcCharging.rankChangingArc {V : Type u_1} (U : Finset V) (b : V → ℤ) (w : Equiv.Perm V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.RankArcCharging.rankChangingArc U b w = {x ∈ U | b (w x) ≠ b x}

theorem SoficGroups.RankArcCharging.card_sdiff_selectedRankSupport {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (b : V → ℤ) (j : Finset V → ℤ) : (U \ selectedRankSupport P b j).card = ∑ C ∈ P.parts, (C.card - {x ∈ C | b x = j C}.card)

theorem SoficGroups.RankArcCharging.rankChangingArc_density_tendsto_zero (V : ℕ → Type u_1) [(n : ℕ) → DecidableEq (V n)] (U : (n : ℕ) → Finset (V n)) (P : (n : ℕ) → Finpartition (U n)) (b : (n : ℕ) → V n → ℤ) (j : (n : ℕ) → Finset (V n) → ℤ) (w : (n : ℕ) → Equiv.Perm (V n)) (N : ℕ → ℝ) (hN : ∀ (n : ℕ), 0 < N n) (hcross : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (P n) (w n)).card / N n) Filter.atTop (nhds 0)) (homit : Filter.Tendsto (fun (n : ℕ) => ↑(U n \ selectedRankSupport (P n) (b n) (j n)).card / N n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(rankChangingArc (U n) (b n) (w n)).card / N n) Filter.atTop (nhds 0)

def SoficGroups.permutationDistance {V : Type u_1} [Fintype V] [DecidableEq V] (p q : Equiv.Perm V) : ℕ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.permutationDistance p q = hammingDist (fun (x : V) => p x) fun (x : V) => q x

@[simp]

theorem SoficGroups.permutationDistance_self {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) : permutationDistance p p = 0

@[simp]

theorem SoficGroups.permutationCommutationDefect_one {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) : permutationCommutationDefect σ 1 = 0

structure SoficGroups.AlmostCentralizerElement {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (tolerance : ℕ) : Type u_1

Internal interface connecting the split non-sofic proof modules.

• permutation : Equiv.Perm V

  Internal interface connecting the split non-sofic proof modules.

• defect_le : permutationCommutationDefect σ self.permutation ≤ tolerance

structure SoficGroups.AlmostCentralizerRepair {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (tolerance : ℕ) : Type u_1

Internal interface connecting the split non-sofic proof modules.

• correct : Equiv.Perm V → Equiv.Perm V

  Internal interface connecting the split non-sofic proof modules.

• corrected_defect (p q : AlmostCentralizerElement σ tolerance) : permutationCommutationDefect σ (self.correct (p.permutation * q.permutation)) ≤ tolerance
• corrected_distance (p q : AlmostCentralizerElement σ tolerance) : 5 * permutationDistance (self.correct (p.permutation * q.permutation)) (p.permutation * q.permutation) ≤ Fintype.card V

structure SoficGroups.HasAlmostCentralizerImprovement {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (tolerance : ℕ) : Prop

Internal interface connecting the split non-sofic proof modules.

• improve (p : Equiv.Perm V) : permutationCommutationDefect σ p ≤ 2 * tolerance → ∃ (q : Equiv.Perm V), permutationCommutationDefect σ q ≤ tolerance ∧ 5 * permutationDistance q p ≤ Fintype.card V

structure SoficGroups.ExpandingCentralizerFiniteModel (G : Type u_1) [Group G] (F : Finset G) : Type (max 1 u_1)

Internal interface connecting the split non-sofic proof modules.

• vertices : Type

  Internal interface connecting the split non-sofic proof modules.

• verticesFintype : Fintype self.vertices

  Internal interface connecting the split non-sofic proof modules.

• verticesDecidableEq : DecidableEq self.vertices

  Internal interface connecting the split non-sofic proof modules.

• generatorIndex : Type

  Internal interface connecting the split non-sofic proof modules.

• generatorFintype : Fintype self.generatorIndex

  Internal interface connecting the split non-sofic proof modules.

• generators : self.generatorIndex → Equiv.Perm self.vertices

  Internal interface connecting the split non-sofic proof modules.

• tolerance : ℕ

  Internal interface connecting the split non-sofic proof modules.

• cheeger : ℝ

  Internal interface connecting the split non-sofic proof modules.

• cheeger_positive : 0 < self.cheeger
• expansion (A : Finset self.vertices) : self.cheeger * min (↑A.card) (↑(Fintype.card self.vertices) - ↑A.card) ≤ ↑(boundary self.generators A)
• small : 10 * ↑self.tolerance < self.cheeger * ↑(Fintype.card self.vertices)
• repair : AlmostCentralizerRepair self.generators self.tolerance

  Internal interface connecting the split non-sofic proof modules.

• approximation : G → AlmostCentralizerElement self.generators self.tolerance

  Internal interface connecting the split non-sofic proof modules.

• map_one : (self.approximation 1).permutation = 1
• multiplicative (x : G) : x ∈ F → ∀ y ∈ F, 5 * permutationDistance (self.approximation (x * y)).permutation ((self.approximation x).permutation * (self.approximation y).permutation) ≤ Fintype.card self.vertices
• separated (x : G) : x ∈ F → ∀ y ∈ F, x ≠ y → Fintype.card self.vertices < 5 * permutationDistance (self.approximation x).permutation (self.approximation y).permutation

noncomputable def SoficGroups.expandingCentralizerFiniteModelOfImprovement {G : Type u_1} [Group G] (F : Finset G) {V ι : Type} [Fintype V] [DecidableEq V] [Fintype ι] (σ : ι → Equiv.Perm V) (tolerance : ℕ) (h : ℝ) (hpositive : 0 < h) (hexp : ∀ (A : Finset V), h * min (↑A.card) (↑(Fintype.card V) - ↑A.card) ≤ ↑(boundary σ A)) (hsmall : 10 * ↑tolerance < h * ↑(Fintype.card V)) (himprove : HasAlmostCentralizerImprovement σ tolerance) (f : G → AlmostCentralizerElement σ tolerance) (hone : (f 1).permutation = 1) (hmul : ∀ x ∈ F, ∀ y ∈ F, 5 * permutationDistance (f (x * y)).permutation ((f x).permutation * (f y).permutation) ≤ Fintype.card V) (hsep : ∀ x ∈ F, ∀ y ∈ F, x ≠ y → Fintype.card V < 5 * permutationDistance (f x).permutation (f y).permutation) : ExpandingCentralizerFiniteModel G F

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.lef_of_expanding_centralizer_models {G : Type u_1} [Group G] (hmodels : ∀ (F : Finset G), Nonempty (ExpandingCentralizerFiniteModel G F)) : LEF G

theorem SoficGroups.exists_positive_antitone_slow_overlap_scales (e : ℕ → ℝ) (he_nonneg : ∀ (n : ℕ), 0 ≤ e n) (he : Filter.Tendsto e Filter.atTop (nhds 0)) : ∃ (eta : ℕ → ℝ) (H : ℕ → ℝ), (∀ (n : ℕ), 0 < eta n) ∧ Antitone eta ∧ Filter.Tendsto eta Filter.atTop (nhds 0) ∧ (∀ (n : ℕ), 0 < H n) ∧ Antitone H ∧ Filter.Tendsto H Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => e n / eta n) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => eta n / H n) Filter.atTop (nhds 0)

theorem SoficGroups.ExceptionalRankOffset.exists_common_log_rank_offsets_tendsto_zero_except (ι : ℕ → Type u_1) [(n : ℕ) → Fintype (ι n)] [(n : ℕ) → DecidableEq (ι n)] (G : (n : ℕ) → Finset (ι n)) (x y : (n : ℕ) → ι n → ℝ) (eta H N : ℕ → ℝ) (C : ℝ) (hx : ∀ (n : ℕ), ∀ i ∈ G n, 0 < x n i) (heta0 : ∀ (n : ℕ), 0 ≤ eta n) (heta1 : ∀ (n : ℕ), eta n < 1) (hH : ∀ (n : ℕ), 0 < H n) (hN : ∀ (n : ℕ), 0 < N n) (hcard : ∀ (n : ℕ), ↑(G n).card ≤ C * N n) (hcomparison : ∀ (n : ℕ), ∀ i ∈ G n, (1 - eta n) * x n i ≤ y n i) (heta : Filter.Tendsto eta Filter.atTop (nhds 0)) (hratio : Filter.Tendsto (fun (n : ℕ) => eta n / H n) Filter.atTop (nhds 0)) (hexceptions : Filter.Tendsto (fun (n : ℕ) => ↑(Finset.univ \ G n).card / N n) Filter.atTop (nhds 0)) : ∃ (r : ℕ → ℝ), (∀ (n : ℕ), r n ∈ Set.Ico 0 (H n)) ∧ Filter.Tendsto (fun (n : ℕ) => rankDropCount (fun (i : ι n) => Real.log (x n i)) (fun (i : ι n) => Real.log (y n i)) (H n) (r n) / N n) Filter.atTop (nhds 0)

noncomputable def SoficGroups.binaryPrefixElementaryGroupEquiv {ι : Type u} [Fintype ι] [DecidableEq ι] (E : BinaryPrefixCode ι) : ↥(elementaryGroup ι BinaryLeavitt) ≃* ↥(prefixElementaryGroup E)

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.CompressionCriterion.normalizedHamming_distinct_tendsto {G : Type u_1} [Group G] (A : SoficApproximation G) {g h : G} (hne : g ≠ h) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((A.model n).action g) ((A.model n).action h)) Filter.atTop (nhds 1)

noncomputable def SoficGroups.CompressionCriterion.productTrackedTable {J : Type u_1} [Group J] (F : Finset J) : Finset J

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CompressionCriterion.productTrackedTable F = SoficGroups.multiplicationTable✝ (insert 1 F)

theorem SoficGroups.CompressionCriterion.one_mem_productTrackedTable {J : Type u_1} [Group J] (F : Finset J) : 1 ∈ productTrackedTable F

theorem SoficGroups.CompressionCriterion.mem_productTrackedTable {J : Type u_1} [Group J] {F : Finset J} {j : J} (hj : j ∈ F) : j ∈ productTrackedTable F

theorem SoficGroups.CompressionCriterion.mul_mem_productTrackedTable {J : Type u_1} [Group J] {F : Finset J} {x y : J} (hx : x ∈ F) (hy : y ∈ F) : x * y ∈ productTrackedTable F

def SoficGroups.permutationGraph {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) : Finset (V × V)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.permutationGraph p = Finset.image (fun (x : V) => (x, p x)) Finset.univ

theorem SoficGroups.mem_permutationGraph {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) (x y : V) : (x, y) ∈ permutationGraph p ↔ y = p x

theorem SoficGroups.boundary_permutationGraph_eq_commutationDefect {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (p : Equiv.Perm V) : boundary (fun (i : ι) => Equiv.prodCongr (σ i) (σ i)) (permutationGraph p) = permutationCommutationDefect σ p

theorem SoficGroups.kazhdan_generator_displacement {G : Type u} {H : Type v} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : KazhdanPair G) (π : UnitaryRepresentation G H) (hfixed : ∀ (η : H), (∀ (g : G), (π g) η = η) → η = 0) (ξ : H) (hξ : ξ ≠ 0) : ∃ g ∈ P.generators, P.kazhdanConstant * ‖ξ‖ ≤ ‖(π g) ξ - ξ‖

structure SoficGroups.ThompsonPrefixInsertion.PrefixWordAction (g : BinaryLeavittˣ) (a b : List (Fin 2)) : Prop

Internal interface connecting the split non-sofic proof modules.

• prefixing : ↑g * leavittWordS a = leavittWordS b
• deletion : leavittWordT a * ↑g⁻¹ = leavittWordT b

theorem SoficGroups.ThompsonPrefixInsertion.prefixWordAction_append {g : BinaryLeavittˣ} {a b : List (Fin 2)} (h : PrefixWordAction g a b) (r : List (Fin 2)) : PrefixWordAction g (a ++ r) (b ++ r)

theorem SoficGroups.ThompsonPrefixInsertion.prefixWordAction_mul {g h : BinaryLeavittˣ} {a b c : List (Fin 2)} (hg : PrefixWordAction g b c) (hh : PrefixWordAction h a b) : PrefixWordAction (g * h) a c

theorem SoficGroups.ThompsonPrefixInsertion.prefixInsertionHom_conjugate_of_prefixWordAction (g : BinaryLeavittˣ) (a b : List (Fin 2)) (h : PrefixWordAction g a b) (u : BinaryLeavittˣ) : g * (prefixInsertionHom a) u * g⁻¹ = (prefixInsertionHom b) u

theorem SoficGroups.ThompsonPrefixInsertion.prefixInsertionHom_mem_binaryPrefixTranspositionGroup (a : List (Fin 2)) (u : BinaryLeavittˣ) (hu : u ∈ binaryPrefixTranspositionGroup) : (prefixInsertionHom a) u ∈ binaryPrefixTranspositionGroup

def SoficGroups.LeavittElementaryMorita.elementaryBlockGroupEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Ring R] [Nontrivial ι] : ↥(elementaryGroup ι (Matrix κ κ R)) ≃* ↥(elementaryGroup (ι × κ) R)

Internal interface connecting the split non-sofic proof modules.

Equations

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

def SoficGroups.LeavittElementaryMorita.elementaryReindexGroupEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Ring R] (e : ι ≃ κ) : ↥(elementaryGroup ι R) ≃* ↥(elementaryGroup κ R)

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.LeavittElementaryMorita.alphaPrefixElementaryGroup_hasPropertyT_of_nine [HasPropertyT (binaryLeavittElementaryGroup 9)] : HasPropertyT ↥(prefixElementaryGroup alphaPrefixCode)

theorem SoficGroups.LeavittElementaryMorita.alphaZeroPrefixElementaryGroup_hasPropertyT_of_nine [HasPropertyT (binaryLeavittElementaryGroup 9)] : HasPropertyT ↥(prefixElementaryGroup alphaZeroPrefixCode)

theorem SoficGroups.ThompsonFiniteGeneration.cylinderSwap_prefixWordAction_of_cases {a b w v : List (Fin 2)} (hab : ¬a <+: b) (hba : ¬b <+: a) (hcase : a <+: w ∧ v = b ++ List.drop a.length w ∨ b <+: w ∧ v = a ++ List.drop b.length w ∨ v = w ∧ ¬a <+: w ∧ ¬w <+: a ∧ ¬b <+: w ∧ ¬w <+: b) : ThompsonPrefixInsertion.PrefixWordAction (ThompsonPrefixInsertion.cylinderSwap a b hab hba) w v