ModularRadonNikodym.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded modular Radon--Nikodym equation

The positive-contraction case of the real pairing equation in Rieffel--van Daele, Pacific Journal of Mathematics 69 (1977), Lemma 4.3, pp.201--202. Weak compactness and polar support tests construct the solution in the original represented algebra.

theorem OAI.KadisonKastler.modular_radon_nikodym_positive line 27

Source documentation

A positive commutant contraction has a self-adjoint contractive solution for every normalized right-half-plane pairing parameter.

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

Mentions: OAI.KadisonKastler.Algebra