OAI/Analysis/KadisonSimilarity/Tracial/NormalRealSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real trace-orthonormal sequence is constructed in the normal source and transported back, so its existence need not be part of a factor model.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.exists_realTracialSequence_of_normal_matrix_tower line 25

    Source documentation

    The fixed matrix source supplies its own real centered sequence.

    theorem exists_realTracialSequence_of_normal_matrix_tower
    (h1 : G.trace 1 = 1) (hf : Function.Injective G.vector)
    (N : VonNeumannAlgebra H) (hN : G.left.range = N.toStarSubalgebra)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop) :
    Nonempty (RealTracialSequence G.trace) := by
…

    Mentions: OAI.KadisonSimilarity.RealTracialSequence