OAI/Analysis/KadisonSimilarity/Derivation/CyclicGraphSequences.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Points of the closed cyclic graph are limits of actual algebra orbits.

  1. theorem OAI.KadisonSimilarity.exists_cyclicGraph_sequence line 17
  2. theorem OAI.KadisonSimilarity.exists_cyclicGraph_coordinate_limits line 37

    Source documentation

    Both coordinates of a graph point are limits of the same algebra orbit.

    theorem exists_cyclicGraph_coordinate_limits
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (Ω : H) (ξ : K) (x : cyclicGraph σ ρ Ω ξ) :
    ∃ a : ℕ → A,
      Tendsto (fun n => σ (a n) Ω) atTop (𝓝 (x : RectangularSum H K).fst) ∧
      Tendsto (fun n => ρ (a n) ξ) atTop (𝓝 (x : RectangularSum H K).snd) := by
…

    Mentions: OAI.KadisonSimilarity.cyclicGraph, OAI.KadisonSimilarity.RectangularSum