StateOrbitGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative gaps from weakly closed state-central unitary orbits

This is the vector estimate in Haagerup, Acta Math. 158 (1987), Lemma 3.2. The scalar orbit-hull hypothesis is the consequence of triviality of the bicentralizer in Proposition 1.3.

def OAI.KadisonKastler.stateUnitaryOrbit line 23

theorem OAI.KadisonKastler.exists_unitary_gap_of_state_orbit_hull line 29

Source documentation

WOT-closed convex hulls cannot cross a closed vector-distance ball unless one of the generating conjugates already does.

theorem exists_unitary_gap_of_state_orbit_hull
    (ξ : H) (a : Algebra M) (δ r : ℝ) (hr : 0 ≤ r)
    (T : H →WOT[ℂ] H) (hT : T ∈ closedConvexHull ℝ (stateUnitaryOrbit ξ a δ))
    (hgap : r < ‖T ξ-a.val ξ‖) :
    ∃ u : unitary (Algebra M), ‖vectorStateCommutator ξ u.val‖ ≤ δ ∧
      r < ‖(u.val*a-a*u.val).val ξ‖ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.stateUnitaryOrbit, OAI.KadisonKastler.vectorStateCommutator

theorem OAI.KadisonKastler.exists_unitary_gap_of_scalar_state_orbit_hull line 75