MatrixFactorDixmier.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact Dixmier averaging in a full finite matrix factor

theorem OAI.KadisonKastler.matrix_size_positive line 16

theorem OAI.KadisonKastler.exists_exact_matrix_factor_average line 26

Source documentation

A full matrix presentation supplies a single exact scalar average.

theorem exists_exact_matrix_factor_average {n : ℕ}
    (E : MatrixUnitSystem (Fin n) (Algebra M)) (hE : Function.Surjective E.hom)
    (x : Algebra M) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ), A.apply x.val = z • (1 : H →L[ℂ] H) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage

theorem OAI.KadisonKastler.publishedDixmierOfFullMatrix line 49
Source documentation
The published conclusion for a represented finite full matrix factor.
```
theorem publishedDixmierOfFullMatrix {n : ℕ}
    (E : MatrixUnitSystem (Fin n) (Algebra M)) (hE : Function.Surjective E.hom) :
    PublishedDixmierAveraging M := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.PublishedDixmierAveraging