Compression arguments for the non-sofic group construction

This file assembles the rooted finite-model and component-compression arguments used by the final contradiction.

theorem SoficGroups.KunRootedWordPower.norm_iterate_sub_le_sum_successive {E : Type u_1} [NormedAddCommGroup E] (F : E → E) (x : E) (k : ℕ) : ‖F^[k] x - x‖ ≤ ∑ j ∈ Finset.range k, ‖F^[j + 1] x - F^[j] x‖

The displacement of an iterate is bounded by its successive displacements.

theorem SoficGroups.MatchedFirstStageWordRadiusTransfer.pruned_sourceCompletionBad_density_tendsto_zero_of_matchedRadius (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} {κ : Type u_3} {J : Type u_4} [Fintype ι] [Group J] (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (p : (n : ℕ) → J → Equiv.Perm (V n)) (F : Finset J) (U P : (n : ℕ) → Finset (V n)) (Q : (n : ℕ) → Finpartition (U n)) (I : ℕ → Finset κ) (w : (n : ℕ) → κ → Equiv.Perm (V n)) (r : ℕ → ℕ) (B : (n : ℕ) → ℕ → Finset (V n)) (D : (n : ℕ) → Finset ↥(P n)) (hcapture : ∀ (n : ℕ), MatchedComponentCompletion.sourceCompletionBad (σ n) (p n) F (P n) ⊆ P n ∩ matchedRadiusBad (Q n) (I (r n)) (w n) (B n (r n))) (hradius : Filter.Tendsto (fun (n : ℕ) => ↑(P n ∩ matchedRadiusBad (Q n) (I (r n)) (w n) (B n (r n))).card / ↑(P n).card) Filter.atTop (nhds 0)) (hZ : ∀ (n : ℕ), (Finset.univ \ D n).Nonempty) (hdeleted : Filter.Tendsto (fun (n : ℕ) => ↑(D n).card / ↑(P n).card) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(MatchedComponentCompletion.sourceCompletionBad (fun (i : ι) => MatchedComponentCompletion.completedRestriction (σ n i) (P n)) (fun (j : J) => MatchedComponentCompletion.completedRestriction (p n j) (P n)) F (Finset.univ \ D n)).card / ↑(Finset.univ \ D n).card) Filter.atTop (nhds 0)

theorem SoficGroups.SourceCompressionMatching.transported_maximumOverlapPart_card_lt_exp_mul {V : Type u_1} [Fintype V] [DecidableEq V] (Q : Finpartition Finset.univ) (T : Equiv.Perm V) (C : Finset V) (hC : C ∈ Q.parts) (H r : ℝ) (hH : 0 < H) (x : V) (hx : x ∈ C) (hTx : T x ∈ maximumOverlapPart Q (Finset.map (Equiv.toEmbedding T) C)) (hrank : MidrankPermutationEnergy.offsetFloorRank (fun (z : V) => Real.log ↑(partitionComponentSize Q z)) H r (T x) = MidrankPermutationEnergy.offsetFloorRank (fun (z : V) => Real.log ↑(partitionComponentSize Q z)) H r x) : ↑(maximumOverlapPart Q (Finset.map (Equiv.toEmbedding T) C)).card < Real.exp H * ↑C.card

theorem SoficGroups.SourceCompressionMatching.symmDiff_card_lt_of_overlap_and_exp_card {V : Type u_1} [DecidableEq V] (C D : Finset V) (H eta : ℝ) (hoverlap : (1 - eta) * ↑C.card ≤ ↑(C ∩ D).card) (hcard : ↑D.card < Real.exp H * ↑C.card) : ↑(symmDiff C D).card < (Real.exp H - 1 + 2 * eta) * ↑C.card

theorem SoficGroups.SourceCompressionMatching.target_majority_of_overlap_and_exp_card {V : Type u_1} [DecidableEq V] (C D : Finset V) (hC : C.Nonempty) (H eta : ℝ) (hoverlap : (1 - eta) * ↑C.card ≤ ↑(C ∩ D).card) (hcard : ↑D.card < Real.exp H * ↑C.card) (hsmall : 2 * (Real.exp H - 1 + 2 * eta) < 1) : D.card < 2 * (C ∩ D).card

theorem SoficGroups.SourceCompressionMatching.symmDiff_density_tendsto_zero_of_log_rank_bounds {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) (D : (n : ℕ) → Finset (V n) → Finset (V n)) (H eta : ℕ → ℝ) (hH : ∀ (n : ℕ), 0 ≤ H n) (heta : ∀ (n : ℕ), 0 ≤ eta n) (hHzero : Filter.Tendsto H Filter.atTop (nhds 0)) (hetazero : Filter.Tendsto eta Filter.atTop (nhds 0)) (hbound : ∀ (n : ℕ), ∀ C ∈ R n, ↑(symmDiff C (D n C)).card ≤ (Real.exp (H n) - 1 + 2 * eta n) * ↑C.card) : Filter.Tendsto (fun (n : ℕ) => ↑(∑ C ∈ R n, (symmDiff C (D n C)).card) / ↑(U n).card) Filter.atTop (nhds 0)

theorem SoficGroups.SourceCompressionTransportCrossing.tendsto_action_inverse {G : Type u_1} [Group G] (A : SoficApproximation G) (u : G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((A.model n).action u)⁻¹ ((A.model n).action u⁻¹)) Filter.atTop (nhds 0)

A sofic approximation preserves inversion asymptotically in normalized Hamming distance.

theorem SoficGroups.SourceCompressionTransportCrossing.tendsto_action_conjugate {G : Type u_1} [Group G] (A : SoficApproximation G) (u g : G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((A.model n).action (u * g * u⁻¹)) ((A.model n).action u * (A.model n).action g * ((A.model n).action u)⁻¹)) Filter.atTop (nhds 0)

theorem SoficGroups.SourceCompressionTransportCrossing.conjugated_word_crossing_density_tendsto_zero {G : Type u_1} [Group G] (A : SoficApproximation G) (u g : G) (Q : (n : ℕ) → Finpartition Finset.univ) (hword : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) ((A.model n).action (u * g * u⁻¹))).card / ↑(A.model n).size) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) ((A.model n).action u * (A.model n).action g * ((A.model n).action u)⁻¹)).card / ↑(A.model n).size) Filter.atTop (nhds 0)

theorem SoficGroups.KunResidualRetainedSelection.exists_matched_slow_diagonal_large_components_on_source_scale_tail {K : Type u_1} [Group K] [Infinite K] [DecidableEq K] (S : Finset K) (hS : 1 ∈ S) (hgen : Subgroup.closure ↑S = ⊤) {V : ℕ → Type u_2} [(n : ℕ) → DecidableEq (V n)] {ι : Type u_3} {κ : Type u_4} [Fintype κ] (σ : (n : ℕ) → κ → Equiv.Perm (V n)) (U : (n : ℕ) → Finset (V n)) (hU : ∀ (n : ℕ), (U n).Nonempty) (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) (H eta : ℕ → ℝ) (hH : Filter.Tendsto H Filter.atTop (nhds 0)) (heta : Filter.Tendsto eta Filter.atTop (nhds 0)) (hmajor : ∀ (n : ℕ), eta n ≤ 1 / 2 → 2 * (Real.exp (H n) - 1 + 2 * eta n) < 1 → ∀ 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)) (hboundary : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, ↑(boundary (σ n) C)) / ↑(U n).card) Filter.atTop (nhds 0)) (hrealize : ∀ (n k : ℕ), ∀ C ∈ R n, ∀ x ∈ C, x ∉ matchedRadiusBad (P n) (I k) (w n) (B n k) → ∃ (f : K → V n), Set.MapsTo f ↑(S ^ (k / 2)) ↑C ∧ Set.InjOn f ↑(S ^ (k / 2))) (N₀ : ℕ) : ∃ (N : ℕ) (r : ℕ → ℕ) (C : (n : ℕ) → Finset (V (n + N))), N₀ ≤ N ∧ (∀ (n : ℕ), eta (n + N) ≤ 1 / 2) ∧ (∀ (n : ℕ), 2 * (Real.exp (H (n + N)) - 1 + 2 * eta (n + N)) < 1) ∧ Filter.Tendsto r Filter.atTop Filter.atTop ∧ (∀ (n : ℕ), C n ∈ R (n + N)) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(boundary (σ (n + N)) (C n)) / ↑(C n).card) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(C n ∩ matchedRadiusBad (P (n + N)) (I (r n)) (w (n + N)) (B (n + N) (r n))).card / ↑(C n).card) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => (C n).card) Filter.atTop Filter.atTop

noncomputable def SoficGroups.SourceCompressionRetainedDiscard.witnesslessComponents {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : Finpartition Finset.univ) (T : Equiv.Perm V) (b : V → ℤ) (eta : ℝ) : Finset (Finset V)

Internal interface connecting the split non-sofic proof modules.

Equations

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

noncomputable def SoficGroups.SourceCompressionRetainedDiscard.retainedComponents {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : Finpartition Finset.univ) (T : Equiv.Perm V) (b : V → ℤ) (eta : ℝ) : Finset (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.SourceCompressionRetainedDiscard.retainedComponents_spec {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : Finpartition Finset.univ) (T : Equiv.Perm V) (b : V → ℤ) (eta : ℝ) (C : Finset V) (hC : C ∈ retainedComponents P Q T b eta) : C ∈ P.parts ∧ maximumOverlapPart Q C ∈ Q.parts ∧ (1 - eta) * ↑C.card ≤ ↑(C ∩ maximumOverlapPart Q C).card ∧ ∃ y ∈ C ∩ maximumOverlapPart Q C, b ((Equiv.symm T) y) = b y

theorem SoficGroups.SourceCompressionRetainedDiscard.retained_missing_density_tendsto_zero (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (P Q : (n : ℕ) → Finpartition Finset.univ) (T : (n : ℕ) → Equiv.Perm (V n)) (b : (n : ℕ) → V n → ℤ) (eta : ℕ → ℝ) (heta : Filter.Tendsto eta Filter.atTop (nhds 0)) (hoverlap : Filter.Tendsto (fun (n : ℕ) => ↑(∑ C ∈ insufficientOverlapComponents (P n) (Q n) (eta n), C.card) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hrank : Filter.Tendsto (fun (n : ℕ) => ↑(RankArcCharging.rankChangingArc Finset.univ (b n) (Equiv.symm (T n))).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(Finset.univ \ matchedRetainedSupport (retainedComponents (P n) (Q n) (T n) (b n) (eta n))).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.SourceGeneratedWordCrossing.sum_generator_crossing_eq_sum_partition_boundary {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] (Q : Finpartition Finset.univ) (σ : ι → Equiv.Perm V) : ∑ i : ι, (partitionWordCrossing Q (σ i)).card = ∑ C ∈ Q.parts, boundary σ C

theorem SoficGroups.SourceGeneratedWordCrossing.generator_crossing_density_tendsto_zero {V : ℕ → Type u_1} [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} [Fintype ι] (Q : (n : ℕ) → Finpartition Finset.univ) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (hboundary : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (Q n).parts, ↑(boundary (σ n) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (i : ι) : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) (σ n i)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.SourceGeneratedWordCrossing.crossing_density_tendsto_zero_of_normalizedHamming {V : ℕ → Type u_1} [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (Q : (n : ℕ) → Finpartition Finset.univ) (p q : (n : ℕ) → Equiv.Perm (V n)) (hq : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) (q n)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hdist : Filter.Tendsto (fun (n : ℕ) => normalizedHamming (p n) (q n)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) (p n)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.SourceGeneratedWordCrossing.fixed_generated_word_crossing_density_tendsto_zero {G : Type u_1} {H : Type u_2} [Group G] [Group H] (A : SoficApproximation G) (φ : H →* G) (S : Finset H) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (Q : (n : ℕ) → Finpartition Finset.univ) (hboundary : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (Q n).parts, ↑(boundary (fun (i : ↥S) => (A.model n).action (φ ↑i)) C)) / ↑(A.model n).size) Filter.atTop (nhds 0)) (g : H) : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) ((A.model n).action (φ g))).card / ↑(A.model n).size) Filter.atTop (nhds 0)

def SoficGroups.SourceGeneratedWordCrossing.sourceAlphaInclusion : ↥(prefixElementaryGroup alphaPrefixCode) →* ↥(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.SourceGeneratedWordCrossing.source_alpha_word_crossing_density_tendsto_zero (A : SoficApproximation ↥(prefixElementaryGroup ninePrefixCode)) (S : Finset ↥(prefixElementaryGroup alphaPrefixCode)) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (Q : (n : ℕ) → Finpartition Finset.univ) (hboundary : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (Q n).parts, ↑(boundary (fun (i : ↥S) => (A.model n).action (sourceAlphaInclusion ↑i)) C)) / ↑(A.model n).size) Filter.atTop (nhds 0)) (g : ↥(prefixElementaryGroup alphaPrefixCode)) : Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) ((A.model n).action (sourceAlphaInclusion g))).card / ↑(A.model n).size) Filter.atTop (nhds 0)

def SoficGroups.SourceBothCompressionNormalization.sourceCompressionUElement : ↥(prefixElementaryGroup ninePrefixCode)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.SourceBothCompressionNormalization.sourceCompressionUElement = ⟨SoficGroups.compressionU, SoficGroups.compressionU_mem_ninePrefixElementaryGroup⟩

def SoficGroups.SourceBothCompressionNormalization.sourceCompressionVElement : ↥(prefixElementaryGroup ninePrefixCode)

The second compression element, regarded as an element of the nine-prefix elementary group.

Equations

• SoficGroups.SourceBothCompressionNormalization.sourceCompressionVElement = ⟨SoficGroups.compressionV, SoficGroups.compressionV_mem_ninePrefixElementaryGroup⟩

@[reducible, inline]

abbrev SoficGroups.SourceBothCompressionNormalization.sourceAlphaElement (g : ↥(prefixElementaryGroup alphaPrefixCode)) : ↥(prefixElementaryGroup ninePrefixCode)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.SourceBothCompressionNormalization.sourceAlphaElement g = SoficGroups.SourceGeneratedWordCrossing.sourceAlphaInclusion g

def SoficGroups.SourceBothCompressionNormalization.sourceCompressionTable : Fin 2 → ↥(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.SourceBothCompressionNormalization.sourceCompressionTable_conjugates_alpha (i : Fin 2) (g : ↥(prefixElementaryGroup alphaPrefixCode)) : ∃ (k : ↥(prefixElementaryGroup alphaPrefixCode)), sourceCompressionTable i * sourceAlphaElement g * (sourceCompressionTable i)⁻¹ = sourceAlphaElement k

theorem SoficGroups.KunTransportedAmbientOverlap.dominant_component_loss_density_tendsto_zero {V : ℕ → Type u_1} [(n : ℕ) → Fintype (V n)] [∀ (n : ℕ), Nonempty (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} [Fintype ι] (P Q : (n : ℕ) → Finpartition Finset.univ) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (gamma : ℝ) (hgamma : 0 < gamma) (hexp : ∀ (n : ℕ), ∀ C ∈ (P n).parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → gamma * ↑E.card ≤ ↑(boundary (σ n) E)) (hsource : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, ↑(boundary (σ n) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (htarget : Filter.Tendsto (fun (n : ℕ) => (∑ D ∈ (Q n).parts, ↑(boundary (σ n) D)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, (↑C.card - ↑(C ∩ maximumOverlapPart (Q n) C).card)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunTransportedAmbientOverlap.transportedUnivFinpartition_half_expansion {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] (Q : Finpartition Finset.univ) (σ : ι → Equiv.Perm V) (T : Equiv.Perm V) (gamma : ℝ) (hexp : ∀ C ∈ Q.parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → gamma * ↑E.card ≤ ↑(boundary σ E)) (C : Finset V) : C ∈ (transportedUnivFinpartition Q T).parts → ∀ E ⊆ C, 2 * E.card ≤ C.card → gamma * ↑E.card ≤ ↑(boundary (fun (i : ι) => T * σ i * T⁻¹) E)

theorem SoficGroups.KunTransportedAmbientOverlap.transported_partition_boundary_density_tendsto_zero {V : ℕ → Type u_1} [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} [Fintype ι] (Q : (n : ℕ) → Finpartition Finset.univ) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (T : (n : ℕ) → Equiv.Perm (V n)) (hboundary : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (Q n).parts, ↑(boundary (σ n) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (transportedUnivFinpartition (Q n) (T n)).parts, ↑(boundary (fun (i : ι) => T n * σ n i * (T n)⁻¹) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunTransportedAmbientOverlap.exists_common_slow_overlap_scales_for_transported_partitions {V : ℕ → Type u_1} [(n : ℕ) → Fintype (V n)] [∀ (n : ℕ), Nonempty (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Finite κ] (Q : (n : ℕ) → Finpartition Finset.univ) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (T : (n : ℕ) → κ → Equiv.Perm (V n)) (gamma : ℝ) (hgamma : 0 < gamma) (hexp : ∀ (n : ℕ), ∀ C ∈ (Q n).parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → gamma * ↑E.card ≤ ↑(boundary (σ n) E)) (hsource : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (Q n).parts, ↑(boundary (σ n) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (htarget : ∀ (j : κ), Filter.Tendsto (fun (n : ℕ) => (∑ D ∈ (Q n).parts, ↑(boundary (fun (i : ι) => T n j * σ n i * (T n j)⁻¹) D)) / ↑(Fintype.card (V n))) 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 : ℕ) => eta n / H n) Filter.atTop (nhds 0) ∧ ∀ (j : κ), Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ insufficientOverlapComponents (transportedUnivFinpartition (Q n) (T n j)) (Q n) (eta n), ↑C.card) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunUniformCompletedRootRadiusImprovement.exists_uniform_radius_hasAlmostCentralizerImprovement {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) (h α : ℝ) (hpositive : 0 < h) (hα : 0 < α) : ∃ (r : ℕ), ∀ (V : Type u) [inst : Fintype V] [Nonempty V] [inst_2 : DecidableEq V] (σ : ↥S → Equiv.Perm V) (φ : G → Equiv.Perm V) (tolerance : ℕ) (B : Finset V), (∀ (g : G), φ g = (List.map σ (w g)).prod) → φ 1 = 1 → (∀ (i : ↥S), φ ↑i = σ i) → (∀ (A : Finset V), h * min (↑A.card) (↑(Fintype.card V) - ↑A.card) ≤ ↑(boundary σ A)) → 5 * (4 + h * (216 / (↑S.card * (1 - KunThomInvariantOrthogonal.kazhdanMarkovContractionFactor P S) ^ 2) + 1 / ↑S.card)) * ↑tolerance ≤ h * ↑(Fintype.card V) → (tolerance = 0 ∨ 0 < ↑tolerance ∧ α ≤ h * ↑tolerance / (2 * (h + 8 * ↑S.card) * ↑(Fintype.card V)) ∧ 2 * ↑S.card * ↑B.card ≤ ↑tolerance ∧ ∀ (a g : G), (w a).length + (w g).length + (w (a * g)).length ≤ r → ∀ x ∉ B, (φ (a * g)) x = (φ a * φ g) x) → HasAlmostCentralizerImprovement σ tolerance

def SoficGroups.CompletedChosenWordLocalRoot.chosenWordEvaluation {G : Type u_1} {ι : Type u_2} {V : Type u_3} (σ : ι → Equiv.Perm V) (w : G → List ι) (g : G) : Equiv.Perm V

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.CompletedChosenWordLocalRoot.chosenWordEvaluation σ w g = (List.map σ (w g)).prod

theorem SoficGroups.CompletedChosenWordLocalRoot.chosenWordEvaluation_multiplicative_tendsto {G : Type u_1} {ι : Type u_2} [Group G] (V : ℕ → Type u_3) [(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)) (s : ι → G) (w : G → List ι) (hw : ∀ (g : G), (List.map s (w g)).prod = g) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (hletter : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => normalizedHamming (σ n i) (p n (s i))) Filter.atTop (nhds 0)) (a g : G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming (chosenWordEvaluation (σ n) w (a * g)) (chosenWordEvaluation (σ n) w a * chosenWordEvaluation (σ n) w g)) Filter.atTop (nhds 0)

theorem SoficGroups.CompletedSourceFinalGeneratorTransfer.surviving_card_ratio_tendsto_one (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (D : (n : ℕ) → Finset (V n)) (hZ : ∀ (n : ℕ), (Finset.univ \ D n).Nonempty) (hdeleted : Filter.Tendsto (fun (n : ℕ) => ↑(D n).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(Finset.univ \ D n).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 1)

theorem SoficGroups.CompletedSourceFinalGeneratorTransfer.deleted_density_relative_survivors (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (D : (n : ℕ) → Finset (V n)) (hZ : ∀ (n : ℕ), (Finset.univ \ D n).Nonempty) (hdeleted : Filter.Tendsto (fun (n : ℕ) => ↑(D n).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ↑(D n).card / ↑(Finset.univ \ D n).card) Filter.atTop (nhds 0)

theorem SoficGroups.CompletedSourceFinalGeneratorTransfer.twiceCompleted_sourceGenerator_normalizedHamming_tendsto_zero (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] {ι : Type u_2} {J : Type u_3} (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (p : (n : ℕ) → J → Equiv.Perm (V n)) (s : ι → J) (P : (n : ℕ) → Finset (V n)) (D : (n : ℕ) → Finset ↥(P n)) (τ : (n : ℕ) → ι → Equiv.Perm ↥(Finset.univ \ D n)) (hsource : ∀ (n : ℕ) (i : ι), σ n i = p n (s i)) (hagrees : ∀ (n : ℕ) (i : ι) (x : ↥(Finset.univ \ D n)), (MatchedComponentCompletion.completedRestriction (σ n i) (P n)) ↑x ∈ Finset.univ \ D n → ↑((τ n i) x) = (MatchedComponentCompletion.completedRestriction (σ n i) (P n)) ↑x) (hZ : ∀ (n : ℕ), (Finset.univ \ D n).Nonempty) (hdeleted : Filter.Tendsto (fun (n : ℕ) => ↑(D n).card / ↑(P n).card) Filter.atTop (nhds 0)) (i : ι) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming (τ n i) (MatchedComponentCompletion.completedRestriction (MatchedComponentCompletion.completedRestriction (p n (s i)) (P n)) (Finset.univ \ D n))) Filter.atTop (nhds 0)

def SoficGroups.CompletedPrescribedSpectralRadiusSchedule.fixedRadiusRootBad {G : Type u_1} {V : Type u_2} [Group G] [DecidableEq G] [Fintype V] [DecidableEq V] (φ : G → Equiv.Perm V) (S : Finset G) (r : ℕ) : 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.CompletedPrescribedSpectralRadiusSchedule.fixedRadiusRootBad_rooted {G : Type u_1} {V : Type u_2} [Group G] [DecidableEq G] [Fintype V] [DecidableEq V] (S : Finset G) (hone : 1 ∈ S) (w : G → List ↥S) (hw : ∀ (a : G), (List.map (fun (i : ↥S) => ↑i) (w a)).prod = a) (φ : G → Equiv.Perm V) (r : ℕ) (a g : G) (hr : (w a).length + (w g).length + (w (a * g)).length ≤ r) (x : V) (hx : x ∉ fixedRadiusRootBad φ S r) : (φ (a * g)) x = (φ a * φ g) x

theorem SoficGroups.CompletedPrescribedSpectralRadiusSchedule.fixedRadiusRootBad_density_tendsto_zero {G : Type u_1} [Group G] [DecidableEq G] (V : ℕ → Type u_2) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (φ : (n : ℕ) → G → Equiv.Perm (V n)) (S : Finset G) (hmul : ∀ (a g : G), Filter.Tendsto (fun (n : ℕ) => normalizedHamming (φ n (a * g)) (φ n a * φ n g)) Filter.atTop (nhds 0)) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(fixedRadiusRootBad (φ n) S r).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunSourceUnconditionalFullDecomposition.exists_source_subgroup_and_ambient_full_finpartition_sequences {G Γ : Type} [Group G] [Group Γ] (A : SoficApproximation G) (f : Γ →* G) (hf : Function.Injective ⇑f) (PΓ : KazhdanPair Γ) (PG : KazhdanPair G) (SΓ : Finset Γ) (SG : Finset G) (honeΓ : 1 ∈ SΓ) (honeG : 1 ∈ SG) (hcoverΓ : PΓ.generators ⊆ SΓ) (hcoverG : PG.generators ⊆ SG) (hsymmetricΓ : ∀ g ∈ SΓ, g⁻¹ ∈ SΓ) (hsymmetricG : ∀ g ∈ SG, g⁻¹ ∈ SG) (hgeneratesΓ : Subgroup.closure ↑SΓ = ⊤) (hgeneratesG : Subgroup.closure ↑SG = ⊤) : ∃ (γΓ : ℝ) (γG : ℝ) (QΓ : (n : ℕ) → Finpartition Finset.univ) (QG : (n : ℕ) → Finpartition Finset.univ), 0 < γΓ ∧ 0 < γG ∧ (∀ (n : ℕ), ∀ C ∈ (QΓ n).parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → γΓ * ↑E.card ≤ ↑(boundary (fun (i : ↥SΓ) => (A.model n).action (f ↑i)) E)) ∧ (∀ (n : ℕ), ∀ C ∈ (QG n).parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → γG * ↑E.card ≤ ↑(boundary (fun (i : ↥SG) => (A.model n).action ↑i) E)) ∧ Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (QΓ n).parts, ↑(boundary (fun (i : ↥SΓ) => (A.model n).action (f ↑i)) C)) / ↑(A.model n).size) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (QG n).parts, ↑(boundary (fun (i : ↥SG) => (A.model n).action ↑i) C)) / ↑(A.model n).size) Filter.atTop (nhds 0)

theorem SoficGroups.KunActualCompressedSourceGroupFoundations.alphaZeroPrefixElementaryGroup_infinite : Infinite ↥(prefixElementaryGroup alphaZeroPrefixCode)

theorem SoficGroups.KunExactKazhdanGeneratorChange.exists_kazhdanPair_with_exact_symmetric_generators {G : Type u} [Group G] [HasPropertyT G] (S : Finset G) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) : ∃ (P : KazhdanPair G), P.generators = S

noncomputable def SoficGroups.KunExactActualSourceAmbientGenerators.sourceAmbientSymmetricGenerators (SΓ : Finset ↥(prefixElementaryGroup alphaPrefixCode)) : Finset ↥(prefixElementaryGroup ninePrefixCode)

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.KunExactActualSourceAmbientGenerators.sourceCompressionTable : Fin 2 → ↥(prefixElementaryGroup ninePrefixCode)

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunExactActualSourceAmbientGenerators.sourceCompressionTable = SoficGroups.SourceBothCompressionNormalization.sourceCompressionTable

def SoficGroups.KunExactActualSourceAmbientGenerators.sourcePositiveGeneratorMap (SΓ : Finset ↥(prefixElementaryGroup alphaPrefixCode)) : ↥SΓ ⊕ Fin 2 → ↥(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.KunUnconditionalActualSourceGeneratorData.exists_unconditional_actual_source_generator_data : ∃ (SΓ : Finset ↥(prefixElementaryGroup alphaPrefixCode)) (PΓ : KazhdanPair ↥(prefixElementaryGroup alphaPrefixCode)) (PG : KazhdanPair ↥(prefixElementaryGroup ninePrefixCode)), 1 ∈ SΓ ∧ (∀ g ∈ SΓ, g⁻¹ ∈ SΓ) ∧ Subgroup.closure ↑SΓ = ⊤ ∧ PΓ.generators = SΓ ∧ 1 ∈ KunExactActualSourceAmbientGenerators.sourceAmbientSymmetricGenerators SΓ ∧ (∀ g ∈ KunExactActualSourceAmbientGenerators.sourceAmbientSymmetricGenerators SΓ, g⁻¹ ∈ KunExactActualSourceAmbientGenerators.sourceAmbientSymmetricGenerators SΓ) ∧ Subgroup.closure ↑(KunExactActualSourceAmbientGenerators.sourceAmbientSymmetricGenerators SΓ) = ⊤ ∧ PG.generators = KunExactActualSourceAmbientGenerators.sourceAmbientSymmetricGenerators SΓ ∧ Function.Injective ⇑SourceGeneratedWordCrossing.sourceAlphaInclusion ∧ Subgroup.closure (Set.range (KunExactActualSourceAmbientGenerators.sourcePositiveGeneratorMap SΓ)) = ⊤

noncomputable def SoficGroups.SourceCommonOffsetMidrankEnergy.componentLogRank {V : Type u_1} [Fintype V] [DecidableEq V] (Q : Finpartition Finset.univ) (H r : ℝ) : 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.SourceCommonComponentRankNoBad.exists_common_positive_component_log_rank_with_vanishing_midrank_energy (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [∀ (n : ℕ), Nonempty (V n)] [(n : ℕ) → DecidableEq (V n)] (ι : Type u_2) (κ : Type u_3) [Fintype ι] [Fintype κ] (Q A : (n : ℕ) → Finpartition Finset.univ) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (T : (n : ℕ) → κ → Equiv.Perm (V n)) (eta H : ℕ → ℝ) (heta0 : ∀ (n : ℕ), 0 ≤ eta n) (heta1 : ∀ (n : ℕ), eta n < 1) (hH : ∀ (n : ℕ), 0 < H n) (heta : Filter.Tendsto eta Filter.atTop (nhds 0)) (hratio : Filter.Tendsto (fun (n : ℕ) => eta n / H n) Filter.atTop (nhds 0)) (hcrossQ : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (Q n) (σ n i)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hoverlap : ∀ (j : κ), Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ insufficientOverlapComponents (transportedUnivFinpartition (Q n) (T n j)) (Q n) (eta n), ↑C.card) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hloss : ∀ (j : κ), Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (transportedUnivFinpartition (Q n) (T n j)).parts, (↑C.card - ↑(C ∩ maximumOverlapPart (Q n) C).card)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hcrossA : Filter.Tendsto (fun (n : ℕ) => (∑ i : ι ⊕ κ, ↑(partitionWordCrossing (A n) (Sum.elim (σ n) (T n) i)).card) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : ∃ (r : ℕ → ℝ), (∀ (n : ℕ), r n ∈ Set.Ico 0 (H n)) ∧ Filter.Tendsto (fun (n : ℕ) => (∑ i : ι ⊕ κ, ↑(MidrankPermutationEnergy.rankDecreasingVertices Finset.univ (SourceCommonOffsetMidrankEnergy.componentLogRank (Q n) (H n) (r n)) (Sum.elim (σ n) (T n) i)).card) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => (∑ i : ι ⊕ κ, ∑ x : V n, (MidrankPermutationEnergy.partitionVertexMidrank (A n) (SourceCommonOffsetMidrankEnergy.componentLogRank (Q n) (H n) (r n)) ((Sum.elim (σ n) (T n) i) x) - MidrankPermutationEnergy.partitionVertexMidrank (A n) (SourceCommonOffsetMidrankEnergy.componentLogRank (Q n) (H n) (r n)) x) ^ 2) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

noncomputable def SoficGroups.KunPositiveWordMidrankEnergy.squaredPermutationEnergy {V : Type u_1} [Fintype V] (f : V → ℝ) (p : Equiv.Perm V) : ℝ

Internal interface connecting the split non-sofic proof modules.

Equations

• SoficGroups.KunPositiveWordMidrankEnergy.squaredPermutationEnergy f p = ∑ x : V, (f (p x) - f x) ^ 2

theorem SoficGroups.KunPositiveWordMidrankEnergy.sum_action_energy_tendsto_zero_of_positive_generator_sum {G : Type u_1} {ι : Type u_2} [Group G] [Fintype ι] (A : SoficApproximation G) (s : ι → G) (hgenerate : Subgroup.closure (Set.range s) = ⊤) (f : (n : ℕ) → Fin (A.model n).size → ℝ) (hf0 : ∀ (n : ℕ) (x : Fin (A.model n).size), 0 ≤ f n x) (hf1 : ∀ (n : ℕ) (x : Fin (A.model n).size), f n x ≤ 1) (hpositive : Filter.Tendsto (fun (n : ℕ) => (∑ i : ι, squaredPermutationEnergy (f n) ((A.model n).action (s i))) / ↑(A.model n).size) Filter.atTop (nhds 0)) (S : Finset G) : Filter.Tendsto (fun (n : ℕ) => (∑ g ∈ S, squaredPermutationEnergy (f n) ((A.model n).action g)) / ↑(A.model n).size) Filter.atTop (nhds 0)

theorem SoficGroups.KunGlobalActualAdditiveMidrankVariance.weighted_component_midrankVariance_tendsto_zero_of_source_half_expansion (V : ℕ → Type u_1) [(n : ℕ) → Fintype (V n)] [∀ (n : ℕ), Nonempty (V n)] [(n : ℕ) → DecidableEq (V n)] (ι : Type u_2) [Fintype ι] (P : (n : ℕ) → Finpartition Finset.univ) (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (b : (n : ℕ) → V n → ℤ) (γ : ℝ) (hγ : 0 < γ) (hexpand : ∀ (n : ℕ), ∀ C ∈ (P n).parts, ∀ E ⊆ C, 2 * E.card ≤ C.card → γ * ↑E.card ≤ ↑(boundary (σ n) E)) (hboundary : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, ↑(boundary (σ n) C)) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (henergy : Filter.Tendsto (fun (n : ℕ) => (∑ i : ι, ∑ x : V n, (MidrankPermutationEnergy.partitionVertexMidrank (P n) (b n) ((σ n i) x) - MidrankPermutationEnergy.partitionVertexMidrank (P n) (b n) x) ^ 2) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, ↑C.card * midrankVariance (componentRankMassList C (b n))) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunCommonRankArcInvariance.exists_common_rank_invariance_of_midrank_variance {V : ℕ → Type u_1} [(n : ℕ) → Fintype (V n)] [∀ (n : ℕ), Nonempty (V n)] [(n : ℕ) → DecidableEq (V n)] {κ : Type u_2} (P : (n : ℕ) → Finpartition Finset.univ) (b : (n : ℕ) → V n → ℤ) (w : (n : ℕ) → κ → Equiv.Perm (V n)) (hvariance : Filter.Tendsto (fun (n : ℕ) => (∑ C ∈ (P n).parts, ↑C.card * midrankVariance (componentRankMassList C (b n))) / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) (hcross : ∀ (i : κ), Filter.Tendsto (fun (n : ℕ) => ↑(partitionWordCrossing (P n) (w n i)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)) : ∃ (j : (n : ℕ) → Finset (V n) → ℤ), (∀ (n : ℕ), ∀ C ∈ (P n).parts, j n C ∈ Finset.image (b n) C ∧ ∀ k ∈ Finset.image (b n) C, componentRankMass C (b n) k ≤ componentRankMass C (b n) (j n C)) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(Finset.univ \ RankArcCharging.selectedRankSupport (P n) (b n) (j n)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0) ∧ ∀ (i : κ), Filter.Tendsto (fun (n : ℕ) => ↑(RankArcCharging.rankChangingArc Finset.univ (b n) (w n i)).card / ↑(Fintype.card (V n))) Filter.atTop (nhds 0)

theorem SoficGroups.KunCommonRankArcInvariance.sofic_action_inverse_normalizedHamming_tendsto_zero {G : Type u_1} [Group G] (A : SoficApproximation G) (g : G) : Filter.Tendsto (fun (n : ℕ) => normalizedHamming ((A.model n).action g)⁻¹ ((A.model n).action g⁻¹)) Filter.atTop (nhds 0)

noncomputable def SoficGroups.ChosenCayleyMatchedComponentRealization.sourceFirstFactorCayleyRadiusBad {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] (A : SoficApproximation (K × J)) (S : Finset K) (hsymmetric : ∀ g ∈ S, g⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (n k : ℕ) : Finset (Fin (A.model n).size)

Internal interface connecting the split non-sofic proof modules.

Equations

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

noncomputable def SoficGroups.CanonicalProductRadiusBadMatchedCapture.sourceProductRadiusLabels {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] [DecidableEq J] (S : Finset K) (F : Finset J) (k : ℕ) : Finset (K × J)

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.CanonicalProductRadiusBadMatchedCapture.firstFactor_mem_sourceProductRadiusLabels {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] [DecidableEq J] (S : Finset K) (F : Finset J) (k : ℕ) {a : K} (ha : a ∈ S ^ k) : (a, 1) ∈ sourceProductRadiusLabels S F k

noncomputable def SoficGroups.CanonicalProductRadiusBadMatchedCapture.canonicalProductRadiusBad {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] [DecidableEq J] (A : SoficApproximation (K × J)) (S : Finset K) (hsymmetric : ∀ a ∈ S, a⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (F : Finset J) (n k : ℕ) : Finset (Fin (A.model n).size)

Internal interface connecting the split non-sofic proof modules.

Equations

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

theorem SoficGroups.CanonicalProductRadiusBadMatchedCapture.canonicalProductRadiusBad_density_tendsto_zero {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] [DecidableEq J] (A : SoficApproximation (K × J)) (S : Finset K) (hsymmetric : ∀ a ∈ S, a⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (F : Finset J) (k : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(canonicalProductRadiusBad A S hsymmetric hgenerates F n k).card / ↑(A.model n).size) Filter.atTop (nhds 0)

theorem SoficGroups.CanonicalProductRadiusBadMatchedCapture.component_exit_mem_partitionWordCrossing {V : Type u_1} [DecidableEq V] {U : Finset V} (P : Finpartition U) (C : Finset V) (hC : C ∈ P.parts) (p : Equiv.Perm V) {x : V} (hx : x ∈ C) (hout : p x ∉ C) : x ∈ partitionWordCrossing P p

theorem SoficGroups.CanonicalProductRadiusBadMatchedCapture.sourceCompletionBad_subset_canonical_matchedRadiusBad {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] [DecidableEq J] (A : SoficApproximation (K × J)) (S : Finset K) (hsymmetric : ∀ a ∈ S, a⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (F : Finset J) (n k : ℕ) {U : Finset (Fin (A.model n).size)} (P : Finpartition U) (C : Finset (Fin (A.model n).size)) (hC : C ∈ P.parts) : MatchedComponentCompletion.sourceCompletionBad (fun (i : ↥S) => (A.model n).action (↑i, 1)) (fun (j : J) => (A.model n).action (1, j)) F C ⊆ C ∩ matchedRadiusBad P (sourceProductRadiusLabels S F k) (A.model n).action (canonicalProductRadiusBad A S hsymmetric hgenerates F n k)

theorem SoficGroups.CanonicalProductRadiusBadMatchedCapture.canonical_source_matched_component_cayley_ball_realization {K : Type u_1} {J : Type u_2} [Group K] [Group J] [DecidableEq K] [DecidableEq J] (A : SoficApproximation (K × J)) (S : Finset K) (honeS : 1 ∈ S) (hsymmetric : ∀ a ∈ S, a⁻¹ ∈ S) (hgenerates : Subgroup.closure ↑S = ⊤) (F : Finset J) (n k : ℕ) {U : Finset (Fin (A.model n).size)} (P : Finpartition U) (C : Finset (Fin (A.model n).size)) (hC : C ∈ P.parts) (x : Fin (A.model n).size) (hx : x ∈ C) (hgood : x ∉ matchedRadiusBad P (sourceProductRadiusLabels S F k) (A.model n).action (canonicalProductRadiusBad A S hsymmetric hgenerates F n k)) : ∃ (f : K → Fin (A.model n).size), Set.MapsTo f ↑(S ^ (k / 2)) ↑C ∧ Set.InjOn f ↑(S ^ (k / 2))

theorem SoficGroups.CompletedSelectedCentralizerPairwiseSource.eventually_completed_sourceCentralizer_table_of_bad_density (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) (Z : (n : ℕ) → Finset (V n)) (hZ : ∀ (n : ℕ), (Z n).Nonempty) (hbad : Filter.Tendsto (fun (n : ℕ) => ↑(MatchedComponentCompletion.sourceCompletionBad (σ n) (p n) F (Z n)).card / ↑(Z n).card) Filter.atTop (nhds 0)) (σZ : (n : ℕ) → ι → Equiv.Perm ↥(Z n)) (hσZ : ∀ (n : ℕ) (i : ι) (x : V n) (hx : x ∈ Z n), (σ n i) x ∈ Z n → ↑((σZ n i) ⟨x, hx⟩) = (σ n i) x) (t : ℕ → ℕ) (ht : ∀ (n : ℕ), 2 * Fintype.card ι * (MatchedComponentCompletion.sourceCompletionBad (σ n) (p n) F (Z n)).card ≤ t n) : ∀ᶠ (n : ℕ) in Filter.atTop, (∀ a ∈ F, ∀ b ∈ F, 5 * permutationDistance (MatchedComponentCompletion.completedRestriction (p n (a * b)) (Z n)) (MatchedComponentCompletion.completedRestriction (p n a) (Z n) * MatchedComponentCompletion.completedRestriction (p n b) (Z n)) ≤ Fintype.card ↥(Z n)) ∧ (∀ a ∈ F, ∀ b ∈ F, a ≠ b → Fintype.card ↥(Z n) < 5 * permutationDistance (MatchedComponentCompletion.completedRestriction (p n a) (Z n)) (MatchedComponentCompletion.completedRestriction (p n b) (Z n))) ∧ ∀ a ∈ CompressionCriterion.productTrackedTable F, permutationCommutationDefect (σZ n) (MatchedComponentCompletion.completedRestriction (p n a) (Z n)) ≤ t n

theorem SoficGroups.KunActualSelectedCentralizerFiniteModel.nonempty_expandingCentralizerFiniteModel_of_selected_completed_sequence {J : Type} [Group J] (F : Finset J) (V : ℕ → Type) [(n : ℕ) → Fintype (V n)] [(n : ℕ) → DecidableEq (V n)] (ι : Type) [Fintype ι] (σ : (n : ℕ) → ι → Equiv.Perm (V n)) (p : (n : ℕ) → J → Equiv.Perm (V n)) (hp : ∀ (n : ℕ), p n 1 = 1) (t : ℕ → ℕ) (h : ℝ) (hpositive : 0 < h) (hdefect : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ∈ CompressionCriterion.productTrackedTable F, permutationCommutationDefect (σ n) (p n j) ≤ t n) (hexp : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (E : Finset (V n)), h * min (↑E.card) (↑(Fintype.card (V n)) - ↑E.card) ≤ ↑(boundary (σ n) E)) (hsmall : ∀ᶠ (n : ℕ) in Filter.atTop, 10 * ↑(t n) < h * ↑(Fintype.card (V n))) (himprove : ∀ᶠ (n : ℕ) in Filter.atTop, HasAlmostCentralizerImprovement (σ n) (t n)) (hmul : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ F, ∀ y ∈ F, 5 * permutationDistance (p n (x * y)) (p n x * p n y) ≤ Fintype.card (V n)) (hsep : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ F, ∀ y ∈ F, x ≠ y → Fintype.card (V n) < 5 * permutationDistance (p n x) (p n y)) : Nonempty (ExpandingCentralizerFiniteModel J F)

theorem SoficGroups.SourceTopLevelCompression.sourceLocalPrefixTranspositionGroup_lef_of_source_finite_models (hmodels : ∀ (A : SoficApproximation ↥(prefixElementaryGroup ninePrefixCode)), Filter.Tendsto (fun (n : ℕ) => (A.model n).size) Filter.atTop Filter.atTop → ∀ (F : Finset ↥(ThompsonPrefixInsertion.localPrefixTranspositionGroup [0, 0, 0, 1])), Nonempty (ExpandingCentralizerFiniteModel (↥(ThompsonPrefixInsertion.localPrefixTranspositionGroup [0, 0, 0, 1])) F)) (hsource : Sofic ↥(prefixElementaryGroup ninePrefixCode)) : LEF ↥(ThompsonPrefixInsertion.localPrefixTranspositionGroup [0, 0, 0, 1])