CenterGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Dixmier averaging yields perturbation estimates for the centers while preserving the contraction bound.

theorem OAI.KadisonKastler.norm_unitaryConj_sub_le_of_commuting_approximant line 17
theorem OAI.KadisonKastler.exists_center_unitBall_approx line 36
Source documentation
A central contraction has a central contraction approximant in the neighbor, with three times any strict bound on the ordinary gap.
```
theorem exists_center_unitBall_approx
    {M N : VonNeumannAlgebra H} (hDixmier : PublishedDixmierAveraging N)
    {r : ℝ} (hgap : kkDistance M N < r) {z : H →L[ℂ] H}
    (hz : z ∈ unitBall (concreteCenter M)) :
    ∃ c ∈ unitBall (concreteCenter N), ‖z - c‖ ≤ 3 * r := by
…
```
Mentions: OAI.KadisonKastler.PublishedDixmierAveraging, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.unitBall, OAI.KadisonKastler.concreteCenter
theorem OAI.KadisonKastler.kkDistance_concreteCenter_le line 71
Source documentation
The center map is Lipschitz with constant three in the ordinary Kadison--Kastler metric, on arbitrary representations.
```
theorem kkDistance_concreteCenter_le
    (M N : VonNeumannAlgebra H) (hM : PublishedDixmierAveraging M)
    (hN : PublishedDixmierAveraging N) :
    kkDistance (concreteCenter M) (concreteCenter N) ≤ 3 * kkDistance M N := by
…
```
Mentions: OAI.KadisonKastler.PublishedDixmierAveraging, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.concreteCenter