OAI/Analysis/HilbertCrouzeix/Calculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HilbertCrouzeix.HolomorphicOn.continuousOn line 16
  2. theorem OAI.HilbertCrouzeix.holomorphic_max_attained line 21
  3. theorem OAI.HilbertCrouzeix.isOpen_poleFreeSet line 29
  4. theorem OAI.HilbertCrouzeix.rationalFunction_holomorphic line 37
  5. theorem OAI.HilbertCrouzeix.rational_max_attained line 45
  6. theorem OAI.HilbertCrouzeix.rational_denominator_isUnit line 51

    Distinct definitions of this name: ComparatorChallenges/HilbertCrouzeix.lean:131 (same statement text; different proof or body). Qualify references as OAI.HilbertCrouzeix.rational_denominator_isUnit@path.

  7. theorem OAI.HilbertCrouzeix.numericalRange_eq_empty line 62
  8. theorem OAI.HilbertCrouzeix.amplification_eq_zero line 69
  9. theorem OAI.HilbertCrouzeix.amplifiedOperator_eq_zero line 76
  10. theorem OAI.HilbertCrouzeix.zeroConclusion line 84

    Distinct definitions of this name: ComparatorChallenges/HilbertCrouzeix.lean:136 (same statement text; different proof or body). Qualify references as OAI.HilbertCrouzeix.zeroConclusion@path.