OAI/Analysis/KadisonKastler/SelfAdjointOutwardCut.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing two-vector cut inequalities to a self-adjoint operator

Finite spectral approximation retains the strict energy inequality. There is no operator-norm bound in the resulting projection theorem.

  1. theorem OAI.KadisonKastler.exists_selfAdjoint_two_vector_projection line 23