OAI/Analysis/KadisonSimilarity/Representation/NormalSpectralTruncation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Vanishing normal trace norm forces any convergent fixed-vector orbit to have zero limit, by cutting off its high left spectrum.

  1. theorem OAI.KadisonSimilarity.norm_limit_le_of_spectral_truncation line 23
  2. theorem OAI.KadisonSimilarity.limit_eq_zero_of_spectral_truncation line 45
  3. theorem OAI.KadisonSimilarity.normal_gns_orbit_limit_eq_zero line 61
  4. theorem OAI.KadisonSimilarity.tracialGeometry_gns_norm_eq line 78

    Source documentation

    Equal trace inner products identify the orbit norms in any tracial geometry with the native GNS orbit norms.

    theorem tracialGeometry_gns_norm_eq
    {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (G : TracialCornerGeometry A E)
    (τ : A →ₚ[ℂ] ℂ) (hτ : ∀ a, τ a = G.trace a)
    (a : A) : ‖gnsTracialVector τ a‖ = ‖G.vector a‖ := by
…

    Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.gnsTracialVector

  5. theorem OAI.KadisonSimilarity.normal_geometry_orbit_limit_eq_zero line 88