OAI/Analysis/HilbertCrouzeix/Definitions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HilbertCrouzeix.Coeff line 14

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:14 (same declaration text).

2. abbrev OAI.HilbertCrouzeix.CoeffSpace line 15

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:15 (same declaration text).

3. def OAI.HilbertCrouzeix.numericalRange line 19

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:19 (same declaration text).

4. def OAI.HilbertCrouzeix.numericalClosure line 22

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:22 (same declaration text).

5. abbrev OAI.HilbertCrouzeix.Amplification line 24

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:24 (same declaration text).

6. def OAI.HilbertCrouzeix.tensorOp line 27

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:27 (same declaration text).

7. def OAI.HilbertCrouzeix.matrixPolynomial line 31

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:31 (same declaration text).

8. def OAI.HilbertCrouzeix.polynomialEval line 34

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:34 (same declaration text).

9. def OAI.HilbertCrouzeix.normSup line 38

   Also declared: ComparatorChallenges/HilbertCrouzeix.lean:38 (same declaration text).

10. def OAI.HilbertCrouzeix.contourIntegral line 41

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:40 (same declaration text).

11. def OAI.HilbertCrouzeix.contourIndex line 45

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:44 (same declaration text).

12. def OAI.HilbertCrouzeix.IsCauchyContour line 48

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:47 (same declaration text).

13. def OAI.HilbertCrouzeix.chosenContour line 54

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:53 (same declaration text).

14. def OAI.HilbertCrouzeix.dunfordIntegral line 59

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:58 (same declaration text).

15. def OAI.HilbertCrouzeix.holomorphicCalculus line 63

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:62 (same declaration text).

16. def OAI.HilbertCrouzeix.matrixUnit line 66

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:65 (same declaration text).

17. def OAI.HilbertCrouzeix.holomorphicEval line 68

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:67 (same declaration text).

18. def OAI.HilbertCrouzeix.contourEval line 73
19. def OAI.HilbertCrouzeix.HolomorphicOn line 78
20. abbrev OAI.HilbertCrouzeix.RationalMatrix line 81

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:71 (same declaration text).

21. def OAI.HilbertCrouzeix.poleFreeSet line 83

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:73 (same declaration text).

22. def OAI.HilbertCrouzeix.rationalFunction line 86

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:76 (same declaration text).

23. def OAI.HilbertCrouzeix.rationalCalculus line 89

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:79 (same declaration text).

24. def OAI.HilbertCrouzeix.rationalEval line 92

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:82 (same declaration text).

25. def OAI.HilbertCrouzeix.PolynomialConclusion line 96
26. def OAI.HilbertCrouzeix.HolomorphicConclusion line 104
27. def OAI.HilbertCrouzeix.RationalConclusion line 115
28. def OAI.HilbertCrouzeix.NonzeroConclusion line 124
29. def OAI.HilbertCrouzeix.ZeroConclusion line 129

    Also declared: ComparatorChallenges/HilbertCrouzeix.lean:85 (same declaration text).

30. def OAI.HilbertCrouzeix.UniformlySharp line 141