OAI/Analysis/KadisonKastler/ResolventCyclicModel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A cyclic spectral isometry for the bounded resolvent

Continuous spectral functions are dense in the scalar L2 space. Their functional-calculus vectors have exactly the same norm, so the map extends to an isometry into the original Hilbert space.

  1. abbrev OAI.KadisonKastler.ResolventCyclicL2 line 22
  2. theorem OAI.KadisonKastler.resolventContinuousVector_norm_L2 line 25
  3. def OAI.KadisonKastler.resolventCyclicIsometry line 43
  4. theorem OAI.KadisonKastler.resolventCyclicIsometry_continuous line 50
  5. theorem OAI.KadisonKastler.resolventCyclicIsometry_one line 56