CenterAlignment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative alignment of the centers

The threefold center gap feeds the constructed abelian embedding theorem. The proved small-gap inclusion lemma makes that embedding onto. Moving the neighbor by the inverse unitary costs at most 900g.

theorem OAI.KadisonKastler.exists_near_unitary_aligning_centers line 25

Source documentation

The center alignment constants in Section 9: 450 for the unitary and 901 for the moved algebra gap.

theorem exists_near_unitary_aligning_centers
    (M N : VonNeumannAlgebra H)
    (hM : PublishedDixmierAveraging M) (hN : PublishedDixmierAveraging N)
    {g : ℝ} (hgap : kkDistance M N < g) (hg : g < 1 / 4000) :
    ∃ w : unitary (H →L[ℂ] H), Conjugates w (concreteCenter M) (concreteCenter N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 450 * g ∧
      kkDistance M (unitaryConjugateAlgebra (star w) N) < 901 * g := by
…

Mentions: OAI.KadisonKastler.PublishedDixmierAveraging, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.concreteCenter, OAI.KadisonKastler.unitaryConjugateAlgebra

theorem OAI.KadisonKastler.exists_common_center_neighbor line 51

Source documentation

The moved pair has literally the same concrete center.

theorem exists_common_center_neighbor
    (M N : VonNeumannAlgebra H)
    (hM : PublishedDixmierAveraging M) (hN : PublishedDixmierAveraging N)
    {g : ℝ} (hgap : kkDistance M N < g) (hg : g < 1 / 4000) :
    ∃ w : unitary (H →L[ℂ] H), ‖(w : H →L[ℂ] H) - 1‖ ≤ 450 * g ∧
      concreteCenter (unitaryConjugateAlgebra (star w) N) = concreteCenter M ∧
      kkDistance M (unitaryConjugateAlgebra (star w) N) < 901 * g := by
…

Mentions: OAI.KadisonKastler.PublishedDixmierAveraging, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.concreteCenter, OAI.KadisonKastler.unitaryConjugateAlgebra