OAI/Analysis/KadisonKastler/TypeICyclicDixmier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite type I averaging in the original representation

  1. theorem OAI.KadisonKastler.publishedDixmierOfFiniteTypeICyclic line 20

    Source documentation

    A finite orthonormal basis in the minimal cyclic representation supplies the full matrix average in the given ambient representation.

    theorem publishedDixmierOfFiniteTypeICyclic (hM : ScalarCenter M)
    (p : AlgebraProjection M) (hp : IsMinimalProjectionIn M p)
    (ξ : H) (hξ : ξ ≠ 0) (hpξ : p.val.val ξ = ξ)
    {n : ℕ} (b : OrthonormalBasis (Fin n) ℂ (typeICyclicSpace M ξ)) :
    PublishedDixmierAveraging M := by
…

    Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.PublishedDixmierAveraging