DixmierImplementerBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Centering an inner implementer by Dixmier averaging

Normalized Dixmier averaging centers self-adjoint implementers while controlling their ambient operator norm.

theorem OAI.KadisonKastler.exists_centered_implementer line 18

theorem OAI.KadisonKastler.exists_bounded_selfAdjoint_split line 66

Source documentation

Self-adjoint centering keeps the algebra/commutant decomposition and bounds both summands by the original ambient implementer.

theorem exists_bounded_selfAdjoint_split (P : VonNeumannAlgebra H)
    (hDixmier : PublishedDixmierAveraging P)
    (h : selfAdjoint (H →L[ℂ] H)) (a : H →L[ℂ] H)
    (ha : a ∈ P) (hb : (h : H →L[ℂ] H) - a ∈ P.commutant) :
    ∃ a' b' : selfAdjoint (H →L[ℂ] H),
      (a' : H →L[ℂ] H) ∈ P ∧ (b' : H →L[ℂ] H) ∈ P.commutant ∧
      h = a' + b' ∧ ‖(a' : H →L[ℂ] H)‖ ≤ 2 * ‖(h : H →L[ℂ] H)‖ ∧
      ‖(b' : H →L[ℂ] H)‖ ≤ 3 * ‖(h : H →L[ℂ] H)‖ := by
…

Mentions: OAI.KadisonKastler.PublishedDixmierAveraging