OAI/Analysis/Crouzeix/NumericalRange.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Compact numerical closure, supremum norms, and spectral containment.

  1. theorem OAI.CrouzeixHilbert.norm_le_of_mem_numericalRange line 20
  2. theorem OAI.CrouzeixHilbert.numericalRange_subset_closedBall line 29
  3. theorem OAI.CrouzeixHilbert.numericalClosure_subset_closedBall line 35
  4. theorem OAI.CrouzeixHilbert.isCompact_numericalClosure line 39
  5. theorem OAI.CrouzeixHilbert.numericalRange_nonempty line 43
  6. theorem OAI.CrouzeixHilbert.numericalClosure_nonempty line 48
  7. theorem OAI.CrouzeixHilbert.numericalRange_eq_empty line 53
  8. theorem OAI.CrouzeixHilbert.supNorm_empty line 61
  9. instance OAI.CrouzeixHilbert.amplificationSubsingleton line 64
  10. theorem OAI.CrouzeixHilbert.zeroConclusion line 73
  11. theorem OAI.CrouzeixHilbert.supNorm_le line 89
  12. theorem OAI.CrouzeixHilbert.supNorm_bddAbove line 98
  13. theorem OAI.CrouzeixHilbert.supNorm_nonneg line 103
  14. theorem OAI.CrouzeixHilbert.norm_le_supNorm line 108
  15. theorem OAI.CrouzeixHilbert.supNorm_mono line 113
  16. theorem OAI.CrouzeixHilbert.supNorm_attained line 120
  17. theorem OAI.CrouzeixHilbert.supNorm_closure line 128
  18. theorem OAI.CrouzeixHilbert.continuous_matrixPolynomial line 146
  19. theorem OAI.CrouzeixHilbert.polynomial_sup_eq_max line 151
  20. theorem OAI.CrouzeixHilbert.operator_lower_bound_of_inner line 162
  21. theorem OAI.CrouzeixHilbert.isUnit_of_inner_lower_bound line 181
  22. theorem OAI.CrouzeixHilbert.spectrum_subset_numericalClosure line 215