OAI/Analysis/NumericalRange/HolomorphicEvaluation.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.aeval_nilpotent line 18
  2. lemma OAI.CompleteCrouzeix.iteratedDeriv_polynomial line 32
  3. lemma OAI.CompleteCrouzeix.taylor_coeff_iteratedDeriv line 43
  4. def OAI.CompleteCrouzeix.scalarJetEval line 52

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

  5. lemma OAI.CompleteCrouzeix.scalarJetEval_polynomial line 55
  6. lemma OAI.CompleteCrouzeix.scalarJetEval_eventuallyEq line 69
  7. lemma OAI.CompleteCrouzeix.nilpotent_resolvent_product line 77
  8. lemma OAI.CompleteCrouzeix.matrix_nilpotent_resolvent line 95
  9. def OAI.CompleteCrouzeix.jetPolynomial line 105
  10. lemma OAI.CompleteCrouzeix.jetPolynomial_eval line 108
  11. lemma OAI.CompleteCrouzeix.analytic_taylor_remainder line 117
  12. lemma OAI.CompleteCrouzeix.scalarJetEval_eq_of_remainder line 136
  13. lemma OAI.CompleteCrouzeix.scalarJetEval_taylor line 151
  14. lemma OAI.CompleteCrouzeix.scalarJetEval_mul line 163
  15. lemma OAI.CompleteCrouzeix.scalarJetEval_add line 189
  16. lemma OAI.CompleteCrouzeix.scalarJetEval_sub line 197
  17. lemma OAI.CompleteCrouzeix.scalarJetEval_const line 205
  18. lemma OAI.CompleteCrouzeix.scalarJetEval_pow line 209
  19. lemma OAI.CompleteCrouzeix.scalarJetEval_polynomial_comp line 218
  20. lemma OAI.CompleteCrouzeix.analytic_first_order_remainder line 231
  21. lemma OAI.CompleteCrouzeix.scalarJetEval_nilpotent_part line 240
  22. lemma OAI.CompleteCrouzeix.scalarJetEval_comp line 254
  23. def OAI.CompleteCrouzeix.primaryEquiv line 280

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:83 (same declaration text).

  24. lemma OAI.CompleteCrouzeix.primaryEquiv_coe line 287
  25. lemma OAI.CompleteCrouzeix.primaryEquiv_symm_lof line 296
  26. def OAI.CompleteCrouzeix.primaryNilpotent line 303

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:90 (same declaration text).

  27. lemma OAI.CompleteCrouzeix.primaryNilpotent_pow line 309
  28. def OAI.CompleteCrouzeix.primaryEval line 320

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:96 (same declaration text).

  29. lemma OAI.CompleteCrouzeix.primaryEval_coe line 325
  30. lemma OAI.CompleteCrouzeix.primary_end_ext line 334
  31. lemma OAI.CompleteCrouzeix.aeval_primary_restrict line 345
  32. lemma OAI.CompleteCrouzeix.primaryEval_polynomial line 367
  33. lemma OAI.CompleteCrouzeix.primaryEval_mul line 374
  34. lemma OAI.CompleteCrouzeix.scalarJetEval_intertwine line 394
  35. lemma OAI.CompleteCrouzeix.primaryEval_on_generalized line 409
  36. lemma OAI.CompleteCrouzeix.primaryEval_mapsTo_generalized line 418
  37. lemma OAI.CompleteCrouzeix.primaryEval_comp line 441
  38. lemma OAI.CompleteCrouzeix.primary_end_ext_spectrum line 468
  39. lemma OAI.CompleteCrouzeix.primaryEval_const line 484
  40. lemma OAI.CompleteCrouzeix.primaryEval_id line 488
  41. lemma OAI.CompleteCrouzeix.primaryEval_sub line 492
  42. lemma OAI.CompleteCrouzeix.primaryEval_eventuallyEq line 502
  43. lemma OAI.CompleteCrouzeix.primaryEval_spectrum_subset line 509
  44. lemma OAI.CompleteCrouzeix.primaryEval_intertwine line 530
  45. lemma OAI.CompleteCrouzeix.primaryEval_similarity line 555