II1Dixmier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KadisonKastler.exists_II1_scalar_average line 23
Source documentation
Move to the constructed tracial representation, average there, and pull the finite list of unitaries back through the isometric algebra equivalence.
```
theorem exists_II1_scalar_average (hM : IsII1Factor M.toStarSubalgebra)
    (x : Algebra M) (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply x.val - z • (1 : H →L[ℂ] H)‖ < ε := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage
theorem OAI.KadisonKastler.publishedDixmierOfII1 line 47
Source documentation
Dixmier averaging holds in every concrete representation of a type II₁ factor, without requiring a tracial vector in that representation.
```
theorem publishedDixmierOfII1 (hM : IsII1Factor M.toStarSubalgebra) :
    PublishedDixmierAveraging M := by
…
```
Mentions: OAI.KadisonKastler.PublishedDixmierAveraging