FiniteTracialDixmier.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar norm averaging in diffuse finite factors

theorem OAI.KadisonKastler.exists_tracial_spectral_scalar_average line 26

Source documentation

Round a finite spectral partition, then average all rounded pieces and their common small remainder in one full matrix algebra.

theorem exists_tracial_spectral_scalar_average
    (Q : CornerPartition (identityProjection M)) (c : Fin Q.size → ℂ)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply (∑ i, c i • (Q.piece i).val.val) - z • (1 : H →L[ℂ] H)‖ < ε := by
…

Mentions: OAI.KadisonKastler.FiniteInnerAverage

theorem OAI.KadisonKastler.exists_tracial_normal_scalar_average line 70
Source documentation
Normal elements of a represented diffuse finite factor have scalar finite averages converging in operator norm.
```
theorem exists_tracial_normal_scalar_average (x : Algebra M) [IsStarNormal x]
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply x.val - z • (1 : H →L[ℂ] H)‖ < ε := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage