OAI/Analysis/KadisonKastler/CornerAngleBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform angle bound in a nearly full Hilbert corner

A projection which loses little of two orthogonal unit vectors keeps both vectors nonzero and keeps their normalized angle away from zero. The determinant estimate avoids introducing trigonometric functions.

  1. theorem OAI.KadisonKastler.projection_corner_inner_bound line 19
  2. theorem OAI.KadisonKastler.projection_corner_angle_determinant line 37