ModularResolventRange.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The bounded Tomita resolvent takes commutant vectors into the algebra

The real Radon--Nikodym equation identifies the orthogonal projection of a commutant vector into the closed Tomita graph. Its first coordinate is the already constructed bounded resolvent.

theorem OAI.KadisonKastler.rescaledGraphProjection_of_modular_pairing line 21
theorem OAI.KadisonKastler.graphResolvent_commutant_selfAdjoint line 68
Source documentation
A self-adjoint commutant vector has an actual bounded algebra representative under the graph resolvent. No modular normalization is used.
```
theorem graphResolvent_commutant_selfAdjoint (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (b : Algebra M.commutant) (hb : IsSelfAdjoint b) :
    ∃ a : Algebra M, IsSelfAdjoint a ∧ ‖a‖ ≤ 1 + ‖b‖ ∧
      graphResolvent M J Ω 1 (b.val Ω) = a.val Ω := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.graphResolvent