OAI/Analysis/KadisonKastler/ResolventVectorMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar vector measures of the bounded Tomita resolvent

The real continuous functional calculus, tested on one Hilbert vector, is a positive functional. Riesz representation supplies the finite measure needed to compare the modular phases and their spectral cuts.

  1. def OAI.KadisonKastler.resolventVectorFunctional line 22
  2. def OAI.KadisonKastler.resolventVectorMeasure line 44
  3. instance OAI.KadisonKastler.resolventVectorMeasure_finite line 47
  4. theorem OAI.KadisonKastler.resolventVectorMeasure_integral line 52
  5. theorem OAI.KadisonKastler.resolventVectorMeasure_mass line 59