OAI/Analysis/NumericalRange/Convexity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompleteCrouzeix.continuous_polynomialValue line 15
  2. theorem OAI.CompleteCrouzeix.numericalRange_image line 22
  3. theorem OAI.CompleteCrouzeix.numericalRange_compact line 30
  4. theorem OAI.CompleteCrouzeix.numericalRange_nonempty line 36
  5. theorem OAI.CompleteCrouzeix.rangeMaximum_attained line 43
  6. lemma OAI.CompleteCrouzeix.linear_sphere_image_eq_ball_image line 63
  7. lemma OAI.CompleteCrouzeix.realThree_complex_kernel line 91
  8. abbrev OAI.CompleteCrouzeix.BlochSpace line 99
  9. def OAI.CompleteCrouzeix.blochLinear line 101
  10. lemma OAI.CompleteCrouzeix.convex_bloch_image line 109
  11. def OAI.CompleteCrouzeix.spinorBloch line 125
  12. lemma OAI.CompleteCrouzeix.spinorBloch_norm_sq line 129
  13. lemma OAI.CompleteCrouzeix.spinorBloch_sphere line 135
  14. lemma OAI.CompleteCrouzeix.exists_spinor_of_sphere line 142
  15. lemma OAI.CompleteCrouzeix.exists_spinor_bloch line 186
  16. def OAI.CompleteCrouzeix.spinorQuadratic line 201
  17. lemma OAI.CompleteCrouzeix.spinorQuadratic_bloch line 204
  18. def OAI.CompleteCrouzeix.spinorRange line 217
  19. lemma OAI.CompleteCrouzeix.spinorRange_eq line 220
  20. lemma OAI.CompleteCrouzeix.convex_spinorRange line 232
  21. lemma OAI.CompleteCrouzeix.orthonormal_pair_norm line 242
  22. lemma OAI.CompleteCrouzeix.quadratic_compression line 250
  23. def OAI.CompleteCrouzeix.operatorNumericalRange line 259
  24. lemma OAI.CompleteCrouzeix.compression_spinor_subset line 262
  25. theorem OAI.CompleteCrouzeix.convex_operatorNumericalRange line 272
  26. theorem OAI.CompleteCrouzeix.numericalRange_convex line 324