OAI/Analysis/KadisonKastler/CompleteCommutantDistance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complete commutator-distance formula

The reflection in each simultaneous commutant orbit has norm at most one. Its commutator is twice the missing orbit component. Finite coefficient duality and weak operator separation therefore give the sharp factor one half.

  1. theorem OAI.KadisonKastler.projection_reflection_norm_le_one line 21
  2. theorem OAI.KadisonKastler.complete_commutator_orbit_bound line 40
  3. theorem OAI.KadisonKastler.exists_commutant_of_completelyBounded line 80

    Source documentation

    The sharp strict commutant approximation, for a possibly nonfaithful star representation of a unital C-star algebra on any Hilbert space.

    theorem exists_commutant_of_completelyBounded
    (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) {e : ℝ} (he : 0 ≤ e)
    (hcb : CompletelyBoundedBy ((innerDerivation T).comp π.toAlgHom.toLinearMap) e)
    {r : ℝ} (hr : e / 2 < r) :
    ∃ D : H →L[ℂ] H, (∀ a, D * π a = π a * D) ∧ ‖D - T‖ < r := by
…

    Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.innerDerivation