OAI/Analysis/KadisonKastler/SelfAdjointProjectionCut.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A projection cut from an almost-central self-adjoint contraction

Finite spectral approximations preserve the strict energy inequality. The finite threshold selection then supplies a projection in the original algebra, with both the reference-vector and test-vector bounds.

  1. theorem OAI.KadisonKastler.exists_selfAdjoint_projection_cut line 24
  2. theorem OAI.KadisonKastler.exists_projection_gap_of_selfAdjoint line 63