OAI/Analysis/KadisonKastler/SpectralCoefficientBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Turning the positive spectral-cut inequality into a lower bound on the actual represented vectors.

  1. theorem OAI.KadisonKastler.projection_inner_eq_norm_sq line 26
  2. theorem OAI.KadisonKastler.spectral_lower_bound_on_vectors line 34