OAI/Analysis/DirectCrouzeix/Convexity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Geometry.sphere_lift line 61
  2. abbrev OAI.DirectCrouzeix.Geometry.Three line 82
  3. def OAI.DirectCrouzeix.Geometry.bloch line 84
  4. theorem OAI.DirectCrouzeix.Geometry.norm_sq_three line 87
  5. theorem OAI.DirectCrouzeix.Geometry.norm_bloch line 90
  6. theorem OAI.DirectCrouzeix.Geometry.bloch_surjective_sphere line 101
  7. def OAI.DirectCrouzeix.Geometry.threeLinear line 132
  8. theorem OAI.DirectCrouzeix.Geometry.threeLinear_ker_ne_bot line 137
  9. def OAI.DirectCrouzeix.Geometry.twoForm line 141
  10. theorem OAI.DirectCrouzeix.Geometry.twoForm_bloch line 144
  11. theorem OAI.DirectCrouzeix.Geometry.convex_twoForm line 160
  12. theorem OAI.DirectCrouzeix.Geometry.orthonormal_pair_norm_sq line 185
  13. theorem OAI.DirectCrouzeix.Geometry.twoForm_inner line 191
  14. theorem OAI.DirectCrouzeix.Geometry.convex_quadratic_range line 201