OAI/Analysis/NumericalRange/Main.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompleteCrouzeix.polynomialValue_smul line 10
2. lemma OAI.CompleteCrouzeix.polynomialAt_smul line 13
3. lemma OAI.CompleteCrouzeix.rangeMaximum_nonneg line 17
4. lemma OAI.CompleteCrouzeix.norm_polynomialValue_le_rangeMaximum line 23
5. theorem OAI.CompleteCrouzeix.complete_crouzeix_bound line 30
6. theorem OAI.CompleteCrouzeix.main line 61

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