PublishedDixmier.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The published Dixmier averaging input

Only the contraction case is retained. Blackadar, Operator Algebras, Definition III.2.5.16 and Theorem III.2.5.18, p. 282 (PDF p. 290), state that the norm-closed convex hull of the unitary conjugates of an element of a von Neumann algebra meets its center. This input contains no comparison between different algebras and no perturbation bound.

Primary text: https://bruceblackadar.com/Mathematics/Cycr.pdf

def OAI.KadisonKastler.innerUnitaryOrbit line 23
def OAI.KadisonKastler.PublishedDixmierAveraging line 28
Source documentation
The published averaging statement used to identify centers.
```
def PublishedDixmierAveraging (N : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonKastler.norm_sub_le_of_closed_convex_orbit line 34
Source documentation
The closed convex hull stays in every closed norm ball containing the orbit. This supplies both bounds needed after Dixmier averaging.
```
theorem norm_sub_le_of_closed_convex_orbit
    (N : VonNeumannAlgebra H) (x c z : H →L[ℂ] H) (r : ℝ)
    (h : ∀ u : unitary (Algebra N), ‖unitaryConj (ambientAlgebraUnitary u) x - c‖ ≤ r)
    (hz : z ∈ closure (convexHull ℝ (innerUnitaryOrbit N x))) : ‖z - c‖ ≤ r := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.ambientAlgebraUnitary, OAI.KadisonKastler.innerUnitaryOrbit
theorem OAI.KadisonKastler.norm_le_of_closed_convex_orbit line 44