OAI/Analysis/KadisonKastler/SpatialProjectionPinching.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pinching a spatial implementer by a commutant projection

  1. theorem OAI.KadisonKastler.exists_projection_reducing_implementer line 17

    Source documentation

    The average with the projection reflection preserves the derivation and its norm bound, and reduces the chosen projection.

    theorem exists_projection_reducing_implementer
    (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) (hTsa : IsSelfAdjoint T)
    (hT : ∀ a ∈ M, T * a - a * T ∈ M)
    (p : H →L[ℂ] H) (hp : IsStarProjection p) (hpM : p ∈ M.commutant) :
    ∃ S : H →L[ℂ] H, IsSelfAdjoint S ∧ ‖S‖ ≤ ‖T‖ ∧
      S - T ∈ M.commutant ∧ Commute p S := by
…