OAI/Analysis/KadisonKastler/ModularPairingComplexification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Complexifying the modular Radon--Nikodym equation

The real equation on self-adjoint tests determines a complex-linear identity on all algebra elements. This is the identity used to identify the bounded Tomita resolvent.

  1. def OAI.KadisonKastler.rightVectorPairing line 20
  2. def OAI.KadisonKastler.leftVectorPairing line 23
  3. theorem OAI.KadisonKastler.rightVectorPairing_star line 26
  4. theorem OAI.KadisonKastler.leftVectorPairing_star line 32
  5. theorem OAI.KadisonKastler.rightVectorPairing_selfAdjoint line 37
  6. theorem OAI.KadisonKastler.leftVectorPairing_commutant line 46
  7. theorem OAI.KadisonKastler.modular_pairing_complex line 58

    Source documentation

    The real pairing equation determines the full complex identity.

    theorem modular_pairing_complex (Ω : H) (b : H →L[ℂ] H)
    (hb : b ∈ M.commutant) (hbs : IsSelfAdjoint b)
    (z : ℂ) (x : Algebra M)
    (hpair : ∀ a : selfAdjoint (Algebra M),
      (inner ℂ (a.val.val Ω) (b Ω)).re =
        (z * inner ℂ (a.val.val Ω) (x.val Ω)).re) :
    ∀ a : Algebra M,
      2 * inner ℂ Ω (a.val (b Ω)) =
        z * inner ℂ Ω (a.val (x.val Ω)) +
          star z * inner ℂ (x.val Ω) (a.val Ω) := by
…

    Mentions: OAI.KadisonKastler.Algebra