OAI/Analysis/Crouzeix/Definitions.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CrouzeixHilbert.Operator line 17

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:16 (same declaration text).

2. abbrev OAI.CrouzeixHilbert.Coeff line 19

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:17 (same declaration text).

3. def OAI.CrouzeixHilbert.numericalRange line 23

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:21 (same declaration text).

4. def OAI.CrouzeixHilbert.numericalClosure line 26

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

5. def OAI.CrouzeixHilbert.supNorm line 28

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:26 (same declaration text).

6. abbrev OAI.CrouzeixHilbert.Amplification line 31

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:29 (same declaration text).

7. def OAI.CrouzeixHilbert.tensorOperator line 34

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:32 (same declaration text).

8. def OAI.CrouzeixHilbert.matrixPolynomial line 38

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:36 (same declaration text).

9. def OAI.CrouzeixHilbert.polynomialEval line 41

   Also declared: ComparatorChallenges/CrouzeixHilbert.lean:39 (same declaration text).

10. structure OAI.CrouzeixHilbert.SmoothContour line 45

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:43 (same declaration text).

11. def OAI.CrouzeixHilbert.SmoothContour.index line 50

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:48 (same declaration text).

12. structure OAI.CrouzeixHilbert.CalculusContour line 54

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:52 (same declaration text).

13. def OAI.CrouzeixHilbert.contourEval line 59

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:57 (same declaration text).

14. def OAI.CrouzeixHilbert.holomorphicEval line 64

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

15. def OAI.CrouzeixHilbert.matrixHolomorphicEval line 70

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:68 (same declaration text).

16. def OAI.CrouzeixHilbert.EntrywiseHolomorphic line 75

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

17. abbrev OAI.CrouzeixHilbert.RationalMatrix line 78

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

18. def OAI.CrouzeixHilbert.PolesOutside line 80

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:78 (same declaration text).

19. def OAI.CrouzeixHilbert.matrixRationalFunction line 83

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:81 (same declaration text).

20. def OAI.CrouzeixHilbert.rationalEval line 86

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:84 (same declaration text).

21. def OAI.CrouzeixHilbert.matrixRationalEval line 89

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:87 (same declaration text).

22. def OAI.CrouzeixHilbert.NonzeroConclusion line 93

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:91 (same declaration text).

23. def OAI.CrouzeixHilbert.ZeroConclusion line 123

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:121 (same declaration text).

24. def OAI.CrouzeixHilbert.SharpConstant line 139

    Also declared: ComparatorChallenges/CrouzeixHilbert.lean:137 (same declaration text).