OAI/Analysis/KadisonKastler/FreeDiagonalCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complementary centered block vanishes on reduced words

  1. theorem OAI.KadisonKastler.centered_compression_word_zero line 18
  2. theorem OAI.KadisonKastler.centered_compression_zero line 56
  3. def OAI.KadisonKastler.tracialDiagonalFockModel line 77

    Source documentation

    The faithful GNS action has the complete structural Fock model once the finite diagonal family generates its algebra.

    def tracialDiagonalFockModel
    (hp : ∀ i a, IsStarProjection (e i a))
    (ho : ∀ i a b, a ≠ b → e i a * e i b = 0)
    (hs : ∀ i, ∑ a, e i a = 1) (hf : ScalarFreeDiagonal τ e)
    (hgen : generatedDiagonal e = ⊤) :
    FreeDiagonalModel (Fin r) (Fin d) (TraceStateHilbert τ) :=
…

    Mentions: OAI.KadisonKastler.ScalarFreeDiagonal, OAI.KadisonKastler.generatedDiagonal, OAI.KadisonKastler.FreeDiagonalModel, OAI.KadisonKastler.TraceStateHilbert