Spectral and finite-model estimates for the non-sofic group construction

This file develops the Hilbert-space, expansion, partition, and completion estimates used in the final obstruction.

theorem SoficGroups.three_pair_sum_norm_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (a b c : H) : ‖a + b‖ ^ 2 + ‖b + c‖ ^ 2 + ‖c + a‖ ^ 2 = ‖a + b + c‖ ^ 2 + (‖a‖ ^ 2 + ‖b‖ ^ 2 + ‖c‖ ^ 2)

A three-vector polarization identity used in the spectral-gap argument.

theorem SoficGroups.alphaPrefixElementaryGroup_hasPropertyT_unconditional : HasPropertyT ↥(prefixElementaryGroup alphaPrefixCode)

theorem SoficGroups.alphaZeroPrefixElementaryGroup_hasPropertyT_unconditional : HasPropertyT ↥(prefixElementaryGroup alphaZeroPrefixCode)

theorem SoficGroups.ninePrefixElementaryGroup_hasPropertyT_unconditional : HasPropertyT ↥(prefixElementaryGroup ninePrefixCode)

theorem SoficGroups.KunThomFiberCoarea.card_entering_eq_card_exiting {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) (A : Finset V) : {x : V | x ∉ A ∧ p x ∈ A}.card = {x ∈ A | p x ∉ A}.card

theorem SoficGroups.KunThomFiberCoarea.permutationGraph_card {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) : (permutationGraph p).card = Fintype.card V

theorem SoficGroups.KunThomFiberCoarea.hasAlmostCentralizerImprovement_of_rooted_reference_cuts {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (tolerance : ℕ) (h : ℝ) (hpositive : 0 < h) (hexp : ∀ (A : Finset V), h * min (↑A.card) (↑(Fintype.card V) - ↑A.card) ≤ ↑(boundary σ A)) (hcut : ∀ (p : Equiv.Perm V), permutationCommutationDefect σ p ≤ 2 * tolerance → ∃ (U : Finset (V × V)), 2 * ((U \ permutationGraph p).card + (permutationGraph p \ U).card) ≤ Fintype.card V ∧ (h + 8 * ↑(Fintype.card ι)) * ↑(boundary (fun (i : ι) => Equiv.prodCongr (σ i) (σ i)) U) ≤ h * ↑tolerance ∧ 5 * (4 * ↑(boundary (fun (i : ι) => Equiv.prodCongr (σ i) (σ i)) U) + h * ↑(U \ permutationGraph p).card) ≤ h * ↑(Fintype.card V)) : HasAlmostCentralizerImprovement σ tolerance

def SoficGroups.KunRootedIndicatorCrossing.indicatorVector {V : Type u_1} (f : V → ℝ) : EuclideanSpace ℂ V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunRootedIndicatorCrossing.indicatorVector f = WithLp.toLp 2 fun (x : V) => ↑(f x)

noncomputable def SoficGroups.KunRootedIndicatorCrossing.permutationMarkov {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : ι → Equiv.Perm V) (ξ : EuclideanSpace ℂ V) : EuclideanSpace ℂ V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunRootedIndicatorCrossing.permutationMarkov p ξ = (↑(Fintype.card ι))⁻¹ • ∑ i : ι, (SoficGroups.KunRootedIndicatorCrossing.permutationUnitary✝ (p i)) ξ

noncomputable def SoficGroups.KunThomInvariantOrthogonal.kazhdanMarkovContractionFactor {G : Type u} [Group G] (P : KazhdanPair G) (S : Finset G) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunThomInvariantOrthogonal.kazhdanMarkovContractionFactor P S = max 0 (1 - P.kazhdanConstant ^ 2 / (4 * ↑S.card))

theorem SoficGroups.KunThomInvariantOrthogonal.kazhdanMarkovContractionFactor_lt_one {G : Type u} [Group G] (P : KazhdanPair G) (S : Finset G) (hS : S.Nonempty) : kazhdanMarkovContractionFactor P S < 1

theorem SoficGroups.KunThomInvariantOrthogonal.kazhdanMarkovContractionFactor_nonneg {G : Type u} [Group G] (P : KazhdanPair G) (S : Finset G) : 0 ≤ kazhdanMarkovContractionFactor P S

structure SoficGroups.KunRootedWordPower.RootedIndicatorMarkovModel (G ι : Type u) : Type (u + 1)

Internal interface connecting the split non-sofic proof modules.

• carrier : Type u

  Internal interface connecting the split non-sofic proof modules.

• fintype : Fintype self.carrier

  Internal interface connecting the split non-sofic proof modules.

• generator : ι → Equiv.Perm self.carrier

  Internal interface connecting the split non-sofic proof modules.

• indicator : self.carrier → ℝ

  Internal interface connecting the split non-sofic proof modules.

• evaluation : G → Equiv.Perm self.carrier

  Internal interface connecting the split non-sofic proof modules.

@[instance_reducible]

instance SoficGroups.KunRootedWordPower.rootedIndicatorMarkovModelFintype {G ι : Type u} (X : RootedIndicatorMarkovModel G ι) : Fintype X.carrier

Equations

• SoficGroups.KunRootedWordPower.rootedIndicatorMarkovModelFintype X = X.fintype

structure SoficGroups.KunRootedWordPower.RootedIndicatorMarkovModel.IsGenerated {G ι : Type u} [Group G] [Fintype ι] (X : RootedIndicatorMarkovModel G ι) (s : ι → G) (w : G → List ι) : Prop

Internal interface connecting the split non-sofic proof modules.

• indicator_mem (x : X.carrier) : X.indicator x = 0 ∨ X.indicator x = 1
• word_evaluation (g : G) : X.evaluation g = (List.map X.generator (w g)).prod
• identity_evaluation : X.evaluation 1 = 1
• generator_evaluation (i : ι) : X.evaluation (s i) = X.generator i

structure SoficGroups.KunRootedWordPower.RootedIndicatorMarkovModel.IsRootedAtRadius {G ι : Type u} [Group G] (X : RootedIndicatorMarkovModel G ι) (w : G → List ι) (r : ℕ) : Prop

Internal interface connecting the split non-sofic proof modules.

• out (a g : G) : (w a).length + (w g).length + (w (a * g)).length ≤ r → ∀ (x : X.carrier), (KunRootedIndicatorCrossing.indicatorVector X.indicator).ofLp x ≠ 0 → (X.evaluation (a * g)) x = (X.evaluation a * X.evaluation g) x

theorem SoficGroups.KunRootedWordPower.exists_rooted_word_radius_markov_iterate_contraction {G : Type u} [Group G] (P : KazhdanPair G) (S : Finset G) (honeS : 1 ∈ S) (hcover : P.generators ⊆ S) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (w : G → List ↥S) (k : ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (r : ℕ), ∀ (X : RootedIndicatorMarkovModel G ↥S), X.IsGenerated (fun (i : ↥S) => ↑i) w → X.IsRootedAtRadius w r → ‖(KunRootedIndicatorCrossing.permutationMarkov X.generator)^[k + 1] (KunRootedIndicatorCrossing.indicatorVector X.indicator) - (KunRootedIndicatorCrossing.permutationMarkov X.generator)^[k] (KunRootedIndicatorCrossing.indicatorVector X.indicator)‖ ≤ (KunThomInvariantOrthogonal.kazhdanMarkovContractionFactor P S ^ k + ε) * ‖KunRootedIndicatorCrossing.permutationMarkov X.generator (KunRootedIndicatorCrossing.indicatorVector X.indicator) - KunRootedIndicatorCrossing.indicatorVector X.indicator‖

noncomputable def SoficGroups.KunActualSoficRootRadius.finiteRootBad {G : Type u_1} [Group G] (M : PermutationModel G) (F : Finset G) : Finset (Fin M.size)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunActualSoficRootRadius.finiteRootBad M F = SoficGroups.KunActualSoficRootRadius.finiteMultiplicationBad✝ M F ∪ SoficGroups.KunActualSoficRootRadius.finiteSeparationBad✝ M F

theorem SoficGroups.KunActualSoficRootRadius.finiteRootBad_density_tendsto_zero {G : Type u_1} [Group G] (A : SoficApproximation G) (F : Finset G) : Filter.Tendsto (fun (n : ℕ) => ↑(finiteRootBad (A.model n) F).card / ↑(A.model n).size) Filter.atTop (nhds 0)

theorem SoficGroups.KunActualSoficRootRadius.finiteRootBad_multiplicative {G : Type u_1} [Group G] (M : PermutationModel G) (F : Finset G) {g h : G} (hg : g ∈ F) (hh : h ∈ F) {x : Fin M.size} (hx : x ∉ finiteRootBad M F) : (M.action (g * h)) x = (M.action g * M.action h) x

theorem SoficGroups.KunActualSoficRootRadius.finiteRootBad_separated {G : Type u_1} [Group G] (M : PermutationModel G) (F : Finset G) {g h : G} (hg : g ∈ F) (hh : h ∈ F) (hne : g ≠ h) {x : Fin M.size} (hx : x ∉ finiteRootBad M F) : (M.action g) x ≠ (M.action h) x

theorem SoficGroups.KunActualSoficRootRadius.normalizedHamming_mul_le {V : Type u_1} [Fintype V] [DecidableEq V] (p p' q q' : Equiv.Perm V) : normalizedHamming (p * q) (p' * q') ≤ normalizedHamming p p' + normalizedHamming q q'

theorem SoficGroups.KunActualSoficRootRadius.approximate_action_list_prod_tendsto {G : Type u_1} [Monoid G] (V : ℕ → Type u_2) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (p : (n : ℕ) → G → Equiv.Perm (V n)) (hone : ∀ (n : ℕ), p n 1 = 1) (hmul : ∀ (a g : G), Filter.Tendsto (fun (n : ℕ) => normalizedHamming (p n (a * g)) (p n a * p n g)) Filter.atTop (nhds 0)) (l : List G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming (p n l.prod) (List.map (p n) l).prod) Filter.atTop (nhds 0)

Approximate multiplicativity of unital monoid maps into permutation groups extends to each fixed finite word. The maps need not preserve multiplication exactly.

theorem SoficGroups.KunActualSoficRootRadius.action_list_prod_tendsto {G : Type u_1} [Group G] (A : SoficApproximation G) (l : List G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((A.model n).action l.prod) (List.map (A.model n).action l).prod) Filter.atTop (nhds 0)

In a sofic approximation, evaluating a fixed product agrees asymptotically with multiplying the individual permutation images.

def SoficGroups.KunActualSoficRootRadius.chosenWordEvaluation {G : Type u_1} {ι : Type u_2} [Group G] (A : SoficApproximation G) (s : ι → G) (w : G → List ι) (n : ℕ) (g : G) : Equiv.Perm (Fin (A.model n).size)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunActualSoficRootRadius.chosenWordEvaluation A s w n g = (List.map (fun (i : ι) => (A.model n).action (s i)) (w g)).prod

theorem SoficGroups.KunActualSoficRootRadius.exists_generator_word_of_symmetric_generates {G : Type u_1} [Group G] (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (g : G) : ∃ (l : List ↥S), (List.map (fun (i : ↥S) => ↑i) l).prod = g

Every element of a group generated by a symmetric finite set is represented by a word whose letters all belong to that set.

noncomputable def SoficGroups.KunActualSoficRootRadius.symmetricGeneratorWord {G : Type u_1} [Group G] [DecidableEq G] (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (g : G) : List ↥S

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunActualSoficRootRadius.symmetricGeneratorWord S hsymmetric hgenerates g = if hone : g = 1 then [] else if hg : g ∈ S then [⟨g, hg⟩] else ⋯.choose

theorem SoficGroups.KunActualSoficRootRadius.symmetricGeneratorWord_prod {G : Type u_1} [Group G] [DecidableEq G] (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (g : G) : (List.map (fun (i : ↥S) => ↑i) (symmetricGeneratorWord S hsymmetric hgenerates g)).prod = g

@[simp]

theorem SoficGroups.KunActualSoficRootRadius.symmetricGeneratorWord_one {G : Type u_1} [Group G] [DecidableEq G] (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) : symmetricGeneratorWord S hsymmetric hgenerates 1 = []

theorem SoficGroups.KunActualSoficRootRadius.symmetricGeneratorWord_generator {G : Type u_1} [Group G] [DecidableEq G] (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (i : ↥S) (hi : ↑i ≠ 1) : symmetricGeneratorWord S hsymmetric hgenerates ↑i = [i]

theorem SoficGroups.KunActualSoficRootRadius.chosen_symmetric_wordEvaluation_one {G : Type u_1} [Group G] [DecidableEq G] (A : SoficApproximation G) (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (n : ℕ) : chosenWordEvaluation A (fun (i : ↥S) => ↑i) (symmetricGeneratorWord S hsymmetric hgenerates) n 1 = 1

theorem SoficGroups.KunActualSoficRootRadius.chosen_symmetric_wordEvaluation_generator {G : Type u_1} [Group G] [DecidableEq G] (A : SoficApproximation G) (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (n : ℕ) (i : ↥S) : chosenWordEvaluation A (fun (j : ↥S) => ↑j) (symmetricGeneratorWord S hsymmetric hgenerates) n ↑i = (A.model n).action ↑i

theorem SoficGroups.KunActualSoficRootRadius.mem_generator_pow_of_chosen_word_length {G : Type u_1} [Group G] [DecidableEq G] (S : Finset G) (hone : 1 ∈ S) (w : G → List ↥S) (hw : ∀ (g : G), (List.map (fun (i : ↥S) => ↑i) (w g)).prod = g) {g : G} {r : ℕ} (hgr : (w g).length ≤ r) : g ∈ S ^ r

noncomputable def SoficGroups.KunActualSoficRootRadius.chosenCayleyRadiusBad {G : Type u_1} [Group G] [DecidableEq G] (A : SoficApproximation G) (S : Finset G) (w : G → List ↥S) (n r : ℕ) : Finset (Fin (A.model n).size)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunActualSoficRootRadius.chosenCayleyRadiusBad A S w n r = SoficGroups.KunActualSoficRootRadius.chosenFiniteRootBad✝ A (fun (i : ↥S) => ↑i) w (S ^ r) n

theorem SoficGroups.KunActualSoficRootRadius.chosenCayleyRadiusBad_density_tendsto_zero {G : Type u_1} [Group G] [DecidableEq G] (A : SoficApproximation G) (S : Finset G) (w : G → List ↥S) (hw : ∀ (g : G), (List.map (fun (i : ↥S) => ↑i) (w g)).prod = g) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(chosenCayleyRadiusBad A S w n r).card / ↑(A.model n).size) Filter.atTop (nhds 0)

theorem SoficGroups.KunActualSoficRootRadius.chosenCayleyRadiusBad_rooted {G : Type u_1} [Group G] [DecidableEq G] (A : SoficApproximation G) (S : Finset G) (hone : 1 ∈ S) (w : G → List ↥S) (hw : ∀ (g : G), (List.map (fun (i : ↥S) => ↑i) (w g)).prod = g) (n r : ℕ) (a g : G) (hword : (w a).length + (w g).length + (w (a * g)).length ≤ r) {x : Fin (A.model n).size} (hx : x ∉ chosenCayleyRadiusBad A S w n r) : (chosenWordEvaluation A (fun (i : ↥S) => ↑i) w n (a * g)) x = (chosenWordEvaluation A (fun (i : ↥S) => ↑i) w n a * chosenWordEvaluation A (fun (i : ↥S) => ↑i) w n g) x

theorem SoficGroups.KunActualSoficRootRadius.chosenCayleyRadiusBad_injective_ball {G : Type u_1} [Group G] [DecidableEq G] (A : SoficApproximation G) (S : Finset G) (w : G → List ↥S) (n r : ℕ) {x : Fin (A.model n).size} (hx : x ∉ chosenCayleyRadiusBad A S w n r) : Set.InjOn (fun (g : G) => ((A.model n).action g) x) ↑(S ^ r)

def SoficGroups.KunDirectedIndicatorJensen.realIndicator {V : Type u_1} [DecidableEq V] (T : Finset V) (x : V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunDirectedIndicatorJensen.realIndicator T x = if x ∈ T then 1 else 0

theorem SoficGroups.KunDirectedIndicatorJensen.realIndicator_eq_zero_or_one {V : Type u_1} [DecidableEq V] (T : Finset V) (x : V) : realIndicator T x = 0 ∨ realIndicator T x = 1

A finite-set indicator takes only the values zero and one.

noncomputable def SoficGroups.KunDirectedIndicatorJensen.realPermutationMarkov {V : Type u_1} {ι : Type u_2} [Fintype ι] (σ : ι → Equiv.Perm V) (f : V → ℝ) (x : V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunDirectedIndicatorJensen.realPermutationMarkov σ f x = (∑ i : ι, f ((Equiv.symm (σ i)) x)) / ↑(Fintype.card ι)

theorem SoficGroups.KunDirectedIndicatorJensen.realPermutationMarkov_indicator_defect_sq_le_boundary {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [Nonempty ι] (σ : ι → Equiv.Perm V) (T : Finset V) : ∑ x : V, (realPermutationMarkov σ (realIndicator T) x - realIndicator T x) ^ 2 ≤ 2 * ↑(boundary σ T) / ↑(Fintype.card ι)

@[reducible, inline]

noncomputable abbrev SoficGroups.KunFinitePermutationMarkovMass.realPermutationMarkov {V : Type u_1} {ι : Type u_2} [Fintype ι] (σ : ι → Equiv.Perm V) (f : V → ℝ) (x : V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunFinitePermutationMarkovMass.realPermutationMarkov σ f x = SoficGroups.KunDirectedIndicatorJensen.realPermutationMarkov σ f x

theorem SoficGroups.KunFinitePermutationMarkovMass.sum_realPermutationMarkov_iterate_indicator {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [Nonempty ι] (σ : ι → Equiv.Perm V) (T : Finset V) (k : ℕ) : ∑ x : V, (realPermutationMarkov σ)^[k] (realIndicator T) x = ↑T.card

theorem SoficGroups.KunFinitePermutationMarkovMass.realPermutationMarkov_iterate_indicator_mem_unitInterval {V : Type u_1} {ι : Type u_2} [DecidableEq V] [Fintype ι] [Nonempty ι] (σ : ι → Equiv.Perm V) (T : Finset V) (k : ℕ) (x : V) : 0 ≤ (realPermutationMarkov σ)^[k] (realIndicator T) x ∧ (realPermutationMarkov σ)^[k] (realIndicator T) x ≤ 1

theorem SoficGroups.KunResidualExpanderDecomposition.boundary_complement {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (A : Finset V) : boundary σ (Finset.univ \ A) = boundary σ A

theorem SoficGroups.KunResidualExpanderDecomposition.exists_expanding_full_finpartition_sequence (ι : Type u_1) [Fintype ι] (V : ℕ → Type u_2) [(n : ℕ) → Fintype (V n)] [∀ (n : ℕ), Nonempty (V n)] [(n : ℕ) → DecidableEq (V n)] (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (B : (n : ℕ) → Finset (V n)) (γ : ℝ) (hγ : 0 < γ) (α : ℕ → ℝ) (hα : ∀ (n : ℕ), 0 ≤ α n) (hαzero : Filter.Tendsto α Filter.atTop (nhds 0)) (hbad : Filter.Tendsto (fun (n : ℕ) => ↑(B n).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (himprove : ∀ (n : ℕ), ∀ T ⊆ Finset.univ \ B n, ↑(boundary (σ n) T) < γ * ↑T.card → ∃ (U : Finset (V n)), 3 * (symmDiff U T).card < T.card ∧ ↑(boundary (σ n) U) ≤ α n * ↑U.card) : ∃ (P : (n : ℕ) → Finpartition Finset.univ), 0 < γ ∧ (∀ (n : ℕ), ∀ C ∈ (P n).parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → γ * ↑E.card ≤ ↑(boundary (σ n) E)) ∧ Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, ↑(boundary (σ n) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunResidualExpanderDecomposition.original_boundary_le_completed_add_component_boundary {V : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (C : Finset V) (τ : ι → Equiv.Perm ↥C) (hτ : ∀ (i : ι) (x : V) (hx : x ∈ C), (σ i) x ∈ C → ↑((τ i) ⟨x, hx⟩) = (σ i) x) (A : Finset ↥C) : boundary σ (Finset.map (Function.Embedding.subtype fun (x : V) => x ∈ C) A) ≤ boundary τ A + boundary σ C

theorem SoficGroups.KunResidualExpanderDecomposition.completed_component_additive_expansion {V : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (C : Finset V) (τ : ι → Equiv.Perm ↥C) (hτ : ∀ (i : ι) (x : V) (hx : x ∈ C), (σ i) x ∈ C → ↑((τ i) ⟨x, hx⟩) = (σ i) x) (γ : ℝ) (hexpand : ∀ E ⊆ C, 2 * E.card ≤ C.card → γ * ↑E.card ≤ ↑(boundary σ E)) (A : Finset ↥C) : γ * min (↑A.card) (↑C.card - ↑A.card) - ↑(boundary σ C) ≤ ↑(boundary τ A)

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

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunDiagonalGoodRootGraphLoss.goodPermutationGraph p B = {z ∈ SoficGroups.permutationGraph p | z.1 ∉ B ∧ z.2 ∉ B}

theorem SoficGroups.KunDiagonalGoodRootGraphLoss.goodPermutationGraph_subset {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) (B : Finset V) : goodPermutationGraph p B ⊆ permutationGraph p

theorem SoficGroups.KunDiagonalGoodRootGraphLoss.card_permutationGraph_sdiff_goodPermutationGraph_le {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) (B : Finset V) : (permutationGraph p \ goodPermutationGraph p B).card ≤ 2 * B.card

theorem SoficGroups.KunDiagonalGoodRootGraphLoss.card_goodPermutationGraph_ge_card_sub_twice_bad {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) (B : Finset V) : ↑(Fintype.card V) - 2 * ↑B.card ≤ ↑(goodPermutationGraph p B).card

theorem SoficGroups.KunDiagonalGoodRootGraphLoss.boundary_goodPermutationGraph_le_commutationDefect_add {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) (p : Equiv.Perm V) (B : Finset V) : boundary (fun (i : ι) => Equiv.prodCongr (σ i) (σ i)) (goodPermutationGraph p B) ≤ permutationCommutationDefect σ p + 2 * Fintype.card ι * B.card

theorem SoficGroups.KunCompletedPrunedComponent.hasAlmostCentralizerImprovement_zero {V : Type u_1} {ι : Type u_2} [Fintype V] [Fintype ι] [DecidableEq V] (σ : ι → Equiv.Perm V) : HasAlmostCentralizerImprovement σ 0

theorem SoficGroups.KunCompletedPrunedComponent.exists_completed_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) (τ : ι → Equiv.Perm ↥(Finset.univ \ B)), 2 * B.card ≤ Fintype.card V ∧ ↑B.card ≤ a * ↑(Fintype.card V) / (γ - ell) ∧ (∀ (i : ι) (x : V) (hx : x ∈ Finset.univ \ B), (σ i) x ∈ Finset.univ \ B → ↑((τ i) ⟨x, hx⟩) = (σ i) x) ∧ ∀ (A : Finset ↥(Finset.univ \ B)), ell * min (↑A.card) (↑(Fintype.card ↥(Finset.univ \ B)) - ↑A.card) ≤ ↑(boundary τ A)

noncomputable def SoficGroups.MatchedComponentCompletion.completedRestriction {V : Type u_1} [Fintype V] (p : Equiv.Perm V) (Z : Finset V) : Equiv.Perm ↥Z

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.MatchedComponentCompletion.completedRestriction p Z = Classical.choose ⋯

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_apply_of_mem {V : Type u_1} [Fintype V] (p : Equiv.Perm V) (Z : Finset V) (x : V) (hx : x ∈ Z) (hp : p x ∈ Z) : ↑((completedRestriction p Z) ⟨x, hx⟩) = p x

@[simp]

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_one {V : Type u_1} [Fintype V] (Z : Finset V) : completedRestriction 1 Z = 1

def SoficGroups.MatchedComponentCompletion.subtypeBad {V : Type u_1} [DecidableEq V] (Z E : Finset V) : Finset ↥Z

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.MatchedComponentCompletion.subtypeBad Z E = {x : ↥Z | ↑x ∈ E}

theorem SoficGroups.MatchedComponentCompletion.card_subtypeBad {V : Type u_1} [DecidableEq V] (Z E : Finset V) : (subtypeBad Z E).card = (Z ∩ E).card

theorem SoficGroups.MatchedComponentCompletion.permutationDistance_le_subtypeBad {V : Type u_1} [DecidableEq V] (Z E : Finset V) (p q : Equiv.Perm ↥Z) (hagrees : ∀ (x : ↥Z), ↑x ∉ E → p x = q x) : permutationDistance p q ≤ (subtypeBad Z E).card

noncomputable def SoficGroups.MatchedComponentCompletion.sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.MatchedComponentCompletion.sourceCompletionBad_subset {V : Type u_1} {ι : Type u_2} {J : Type u_3} [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) : sourceCompletionBad σ p F Z ⊆ Z

theorem SoficGroups.MatchedComponentCompletion.card_subtype_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) : (subtypeBad Z (sourceCompletionBad σ p F Z)).card = (sourceCompletionBad σ p F Z).card

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_mul_of_not_mem_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) {j k : J} (hj : j ∈ F) (hk : k ∈ F) (z : ↥Z) (hz : ↑z ∉ sourceCompletionBad σ p F Z) : (completedRestriction (p (j * k)) Z) z = (completedRestriction (p j) Z * completedRestriction (p k) Z) z

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_ne_of_not_mem_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) {j k : J} (hj : j ∈ F) (hk : k ∈ F) (hne : j ≠ k) (z : ↥Z) (hz : ↑z ∉ sourceCompletionBad σ p F Z) : (completedRestriction (p j) Z) z ≠ (completedRestriction (p k) Z) z

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_commute_of_not_mem_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) (σZ : ι → Equiv.Perm ↥Z) (hσZ : ∀ (i : ι) (x : V) (hx : x ∈ Z), (σ i) x ∈ Z → ↑((σZ i) ⟨x, hx⟩) = (σ i) x) {j : J} (hj : j ∈ CompressionCriterion.productTrackedTable F) (i : ι) (z : ↥Z) (hz : ↑z ∉ sourceCompletionBad σ p F Z) : (completedRestriction (p j) Z) ((σZ i) z) = (σZ i) ((completedRestriction (p j) Z) z)

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_mul_distance_le_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) {j k : J} (hj : j ∈ F) (hk : k ∈ F) : permutationDistance (completedRestriction (p (j * k)) Z) (completedRestriction (p j) Z * completedRestriction (p k) Z) ≤ (sourceCompletionBad σ p F Z).card

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_separated_of_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) (hZ : Z.Nonempty) (hbad : 5 * (sourceCompletionBad σ p F Z).card ≤ Z.card) {j k : J} (hj : j ∈ F) (hk : k ∈ F) (hne : j ≠ k) : Fintype.card ↥Z < 5 * permutationDistance (completedRestriction (p j) Z) (completedRestriction (p k) Z)

theorem SoficGroups.MatchedComponentCompletion.completedRestriction_commutationDefect_le_sourceCompletionBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) (σZ : ι → Equiv.Perm ↥Z) (hσZ : ∀ (i : ι) (x : V) (hx : x ∈ Z), (σ i) x ∈ Z → ↑((σZ i) ⟨x, hx⟩) = (σ i) x) {j : J} (hj : j ∈ CompressionCriterion.productTrackedTable F) : permutationCommutationDefect σZ (completedRestriction (p j) Z) ≤ Fintype.card ι * (sourceCompletionBad σ p F Z).card

theorem SoficGroups.MatchedComponentExitBudget.card_permutation_exit_le_deleted {V : Type u_1} [Fintype V] [DecidableEq V] (p : Equiv.Perm V) (Z : Finset V) : {x ∈ Z | p x ∉ Z}.card ≤ (Finset.univ \ Z).card

noncomputable def SoficGroups.MatchedComponentExitBudget.sourceWordTestBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) : Finset V

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.MatchedComponentExitBudget.sourceCompletionBad_subset_exit_union_wordBad {V : Type u_1} {ι : Type u_2} {J : Type u_3} [Fintype V] [DecidableEq V] [Fintype ι] [Group J] (σ : ι → Equiv.Perm V) (p : J → Equiv.Perm V) (F : Finset J) (Z : Finset V) : MatchedComponentCompletion.sourceCompletionBad σ p F Z ⊆ (((Finset.univ.biUnion fun (i : ι) => {z ∈ Z | (σ i) z ∉ Z}) ∪ (CompressionCriterion.productTrackedTable F).biUnion fun (j : J) => {z ∈ Z | (p j) z ∉ Z}) ∪ Finset.univ.biUnion fun (i : ι) => (CompressionCriterion.productTrackedTable F).biUnion fun (j : J) => {z ∈ Z | (p j) ((σ i) z) ∉ Z}) ∪ sourceWordTestBad σ p F

theorem SoficGroups.MatchedComponentExitBudget.sourceCompletionBad_surviving_density_tendsto_zero (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} {J : Type u_3} [Fintype ι] [Group J] (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (p : (n : ℕ) → J → Equiv.Perm (V n)) (F : Finset J) (B : (n : ℕ) → Finset (V n)) (hZ : ∀ (n : ℕ), (Finset.univ \ B n).Nonempty) (hdeleted : Filter.Tendsto (fun (n : ℕ) => ↑(B n).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hword : Filter.Tendsto (fun (n : ℕ) => ↑(sourceWordTestBad (σ n) (p n) F).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(MatchedComponentCompletion.sourceCompletionBad (σ n) (p n) F (Finset.univ \ B n)).card / ↑(Finset.univ \ B n).card) Filter.atTop (nhds 0)

theorem SoficGroups.MatchedComponentExitBudget.pruned_component_card_tendsto_atTop (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (B : (n : ℕ) → Finset (V n)) (hsize : Filter.Tendsto (fun (n : ℕ) => Fintype.card (V n)) Filter.atTop Filter.atTop) (hdeleted : Filter.Tendsto (fun (n : ℕ) => ↑(B n).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (Finset.univ \ B n).card) Filter.atTop Filter.atTop

@[reducible, inline]

noncomputable abbrev SoficGroups.KunRealComplexMarkovBridge.realMarkov {ι : Type u_1} {V : Type u_2} [Fintype ι] (p : ι → Equiv.Perm V) (f : V → ℝ) (x : V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunRealComplexMarkovBridge.realMarkov p f x = SoficGroups.KunDirectedIndicatorJensen.realPermutationMarkov p f x

@[reducible, inline]

abbrev SoficGroups.KunRealComplexMarkovBridge.indicatorVector {V : Type u_1} (f : V → ℝ) : EuclideanSpace ℂ V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunRealComplexMarkovBridge.indicatorVector f = SoficGroups.KunRootedIndicatorCrossing.indicatorVector f

@[reducible, inline]

noncomputable abbrev SoficGroups.KunRealComplexMarkovBridge.permutationMarkov {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : ι → Equiv.Perm V) (ξ : EuclideanSpace ℂ V) : EuclideanSpace ℂ V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunRealComplexMarkovBridge.permutationMarkov p ξ = SoficGroups.KunRootedIndicatorCrossing.permutationMarkov p ξ

theorem SoficGroups.KunRealComplexMarkovBridge.norm_permutationMarkov_indicator_sub_sq {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : ι → Equiv.Perm V) (f : V → ℝ) : ‖permutationMarkov p (indicatorVector f) - indicatorVector f‖ ^ 2 = ∑ x : V, (realMarkov p f x - f x) ^ 2

theorem SoficGroups.KunRealComplexMarkovBridge.norm_iterate_permutationMarkov_indicator_sub_sq {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : ι → Equiv.Perm V) (f : V → ℝ) (k : ℕ) : ‖(permutationMarkov p)^[k] (indicatorVector f) - indicatorVector f‖ ^ 2 = ∑ x : V, ((realMarkov p)^[k] f x - f x) ^ 2

theorem SoficGroups.KunRealComplexMarkovBridge.norm_iterate_permutationMarkov_indicator_sub_iterate_sq {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : ι → Equiv.Perm V) (f : V → ℝ) (k : ℕ) : ‖(permutationMarkov p)^[k + 1] (indicatorVector f) - (permutationMarkov p)^[k] (indicatorVector f)‖ ^ 2 = ∑ x : V, ((realMarkov p)^[k + 1] f x - (realMarkov p)^[k] f x) ^ 2