MatrixOrbitAverage.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar averaging inside a full finite matrix algebra

theorem OAI.KadisonKastler.finiteAverage_mem_convexHull line 20
Source documentation
Uniform finite averages belong to the real convex hull of their values.
```
theorem finiteAverage_mem_convexHull (f : G → V) :
    finiteAverage f ∈ convexHull ℝ (Set.range f) := by
…
```
Mentions: OAI.KadisonKastler.finiteAverage

theorem OAI.KadisonKastler.matrixUnits_scalar_of_mem_of_commutes line 43

Source documentation

The center of a concrete full matrix algebra consists of scalars.

theorem matrixUnits_scalar_of_mem_of_commutes
    (E : MatrixUnitSystem ι (H →L[ℂ] H))
    (x : H →L[ℂ] H) (hx : x ∈ E.algebra)
    (hc : ∀ i j, Commute (E.entry i j) x) :
    ∃ z : ℂ, x = z • (1 : H →L[ℂ] H) := by
…

theorem OAI.KadisonKastler.matrixUnitAverage_scalar line 63
Source documentation
Averaging over the finite signed group sends its whole matrix algebra into the ambient scalar operators.
```
theorem matrixUnitAverage_scalar (E : MatrixUnitSystem ι (H →L[ℂ] H))
    (x : H →L[ℂ] H) (hx : x ∈ E.algebra) :
    ∃ z : ℂ, matrixUnitAverage E x = z • (1 : H →L[ℂ] H) := by
…
```
Mentions: OAI.KadisonKastler.matrixUnitAverage

theorem OAI.KadisonKastler.matrixUnitAverage_mem_orbitHull line 78

Source documentation

The same average lies in the actual ambient unitary orbit hull.

theorem matrixUnitAverage_mem_orbitHull (E : MatrixUnitSystem ι (H →L[ℂ] H))
    (M : VonNeumannAlgebra H) (hE : E.algebra ≤ M.toStarSubalgebra)
    (x : H →L[ℂ] H) :
    matrixUnitAverage E x ∈ convexHull ℝ (innerUnitaryOrbit M x) := by
…

Mentions: OAI.KadisonKastler.matrixUnitAverage, OAI.KadisonKastler.innerUnitaryOrbit