OAI/Analysis/KadisonKastler/ModularRadonSelfAdjoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The modular pairing equation for arbitrary self-adjoint commutant elements

  1. theorem OAI.KadisonKastler.modular_radon_nikodym_nonnegative line 15
  2. theorem OAI.KadisonKastler.modular_radon_nikodym_selfAdjoint line 59

    Source documentation

    The exact real pairing conclusion needed for bounded Tomita resolvents.

    theorem modular_radon_nikodym_selfAdjoint (Ω : H) (b : Algebra M.commutant)
    (hb : IsSelfAdjoint b) (z : ℂ) (hz : 0 < z.re) :
    ∃ x : Algebra M, IsSelfAdjoint x ∧ ‖x‖ ≤ 2 * (1 + ‖b‖) / z.re ∧
      ∀ a : selfAdjoint (Algebra M),
        (inner ℂ (a.val.val Ω) (b.val Ω)).re =
          (z * inner ℂ (a.val.val Ω) (x.val Ω)).re := by
…

    Mentions: OAI.KadisonKastler.Algebra