OAI/Analysis/KadisonKastler/ModularRadonScaling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full right-half-plane parameter in the modular pairing equation

  1. theorem OAI.KadisonKastler.modular_radon_nikodym_positive_halfPlane line 16

    Source documentation

    Rescaling the normalized pairing keeps an explicit operator norm bound.

    theorem modular_radon_nikodym_positive_halfPlane (Ω : H) (b : H →L[ℂ] H)
    (hb : b ∈ M.commutant) (hb0 : 0 ≤ b) (hb1 : b ≤ 1)
    (z : ℂ) (hz : 0 < z.re) :
    ∃ x : Algebra M, IsSelfAdjoint x ∧ ‖x‖ ≤ 1 / z.re ∧
      ∀ a : selfAdjoint (Algebra M),
        (inner ℂ (a.val.val Ω) (b Ω)).re =
          (z * inner ℂ (a.val.val Ω) (x.val Ω)).re := by
…

    Mentions: OAI.KadisonKastler.Algebra