Predecessors.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.sequence_predecessors line 20

theorem OAI.NuclearUltrapower.periodic_of_finite_matches line 92

Source documentation

The finite predecessor graph forces periodicity of every matched irreducible, including the initial vertex even if it lies on a nonempty tail.

theorem periodic_of_finite_matches
    (hf : (matchClasses ρ S u a).Finite)
    (hp : ∀ π : FiniteUnitaryRep.{u,v} Γ, π.Irreducible → Matches ρ S u a π →
      ∃ τ : FiniteUnitaryRep.{u,v} Γ, τ.Irreducible ∧ Matches ρ S u a τ ∧ π.Embeds (τ.pull θ))
    (π : FiniteUnitaryRep.{u,v} Γ) (hπ : π.Irreducible) (hm : Matches ρ S u a π) :
    ∃ p : ℕ, 0 < p ∧ π.Equivalent (π.pull (θ^p)) := by
…

Mentions: OAI.NuclearUltrapower.matchClasses, OAI.NuclearUltrapower.Matches

theorem OAI.NuclearUltrapower.uniform_predecessors line 135

Source documentation

Uniformity is extracted by selecting a bad representation at every bad coordinate. The selected dimensions are not bounded.

theorem uniform_predecessors (κ a : ℝ) (hgap : HasKazhdanGap.{u,u} S κ)
    (hS : Subgroup.closure (S : Set Γ) = ⊤) (ha : a < κ) (ha0 : 0 < a)
    (ht : ∀ g, f (θ g) * t = t * f g)
    (hω : ∀ n : ℕ, ({n} : Set ℕ) ∉ (ω : Filter ℕ))
    (h1 : ∀ n, u 1 n = 1)
    (hmul : ∀ g h, Tendsto (fun n => ‖(u (g*h) n : B) - (u g n : B)*(u h n : B)‖)
      (ω : Filter ℕ) (𝓝 0))
    (π₀ : FiniteUnitaryRep.{u,u} Γ) (hirr₀ : π₀.Irreducible) :
    ∀ᶠ n in (ω : Filter ℕ), ∀ π : FiniteUnitaryRep.{u,u} Γ,
      π.Irreducible → Matches ρ S (fun g => u (f g) n) a π →
      ∃ τ : FiniteUnitaryRep.{u,u} Γ, τ.Irreducible ∧
        Matches ρ S (fun g => u (f g) n) a τ ∧ π.Embeds (τ.pull θ) := by
…

Mentions: OAI.NuclearUltrapower.Matches

theorem OAI.NuclearUltrapower.contradiction_of_initial_match line 177

Source documentation

The finite-match mechanism excludes an aperiodic irrep appearing in the ultrapower spectral support.

theorem contradiction_of_initial_match (κ a : ℝ)
    (hB : IsNuclear.{u,u} B) (hSne : S.Nonempty)
    (hκ0 : 0 < κ) (hκ : κ ≤ 4 * (S.card : ℝ))
    (hgap : HasKazhdanGap.{u,u} S κ) (hS : Subgroup.closure (S : Set Γ) = ⊤)
    (ha : a < κ) (ha0 : 0 < a) (ha' : a < κ^2 / (4 * (S.card : ℝ)))
    (ht : ∀ g, f (θ g) * t = t * f g)
    (hω : ∀ n : ℕ, ({n} : Set ℕ) ∉ (ω : Filter ℕ))
    (h1 : ∀ n, u 1 n = 1)
    (hmul : ∀ g h, Tendsto (fun n => ‖(u (g*h) n : B) - (u g n : B)*(u h n : B)‖)
      (ω : Filter ℕ) (𝓝 0))
    (π : FiniteUnitaryRep.{u,u} Γ) (hirr : π.Irreducible)
    (haper : ∀ p : ℕ, 0 < p → ¬ π.Equivalent (π.pull (θ^p)))
…