TypeIIIDixmier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KadisonKastler.matrixInnerAverage line 20
Source documentation
The finite signed matrix group, considered as inner automorphisms of M.
```
def matrixInnerAverage {n : ℕ} (E : MatrixUnitSystem (Fin n) (H →L[ℂ] H))
    (hE : E.algebra ≤ M.toStarSubalgebra) : FiniteInnerAverage M where
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage
theorem OAI.KadisonKastler.TypeIIIFactor.exists_selfAdjoint_scalar_average line 30
Source documentation
A finite inner average brings a self-adjoint element arbitrarily close to a scalar, by averaging its actual spectral matrix approximation.
```
theorem TypeIIIFactor.exists_selfAdjoint_scalar_average (hM : TypeIIIFactor M)
    (x : Algebra M) (hx : IsSelfAdjoint x) (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply x.val - z • (1 : H →L[ℂ] H)‖ < ε := by
…
```
Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage