OAI/Analysis/KadisonKastler/ProjectionVectorDomination.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Detecting failure of vector-state domination on a projection

Finite positive spectral approximation extends inequalities on projections to positive operators. Consequently a failure of bounded orbit domination is witnessed on a genuine algebra projection, at any prescribed ratio.

  1. theorem OAI.KadisonKastler.vector_quadratic_bound_of_projection_bound line 30
  2. theorem OAI.KadisonKastler.exists_projection_large_vector_ratio line 71