OAI/Analysis/NumericalRange/ExteriorKernel.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompleteCrouzeix.exteriorCorrection_analytic_right line 12
  2. theorem OAI.CompleteCrouzeix.exteriorCorrection_eq line 21
  3. lemma OAI.CompleteCrouzeix.exteriorCorrection_eq_left line 37
  4. theorem OAI.CompleteCrouzeix.exteriorCorrection_analytic_left line 64
  5. lemma OAI.CompleteCrouzeix.dslope_comm line 79
  6. lemma OAI.CompleteCrouzeix.deriv_dslope_eq_iterated line 86
  7. def OAI.CompleteCrouzeix.exteriorDividedDifference line 105
  8. def OAI.CompleteCrouzeix.reciprocalCorrection line 108
  9. lemma OAI.CompleteCrouzeix.reciprocalCorrection_zero_left line 111
  10. lemma OAI.CompleteCrouzeix.reciprocalCorrection_zero_right line 114
  11. lemma OAI.CompleteCrouzeix.reciprocalCorrection_eq_deriv line 117
  12. lemma OAI.CompleteCrouzeix.reciprocalCorrection_analytic_left line 125
  13. lemma OAI.CompleteCrouzeix.reciprocalCorrection_analytic_right line 142
  14. lemma OAI.CompleteCrouzeix.hasDerivAt_exteriorMap line 158
  15. lemma OAI.CompleteCrouzeix.dslope_exteriorMap line 165
  16. lemma OAI.CompleteCrouzeix.dividedDifference_ne_zero line 181
  17. lemma OAI.CompleteCrouzeix.analyticOnNhd_unit_circleAverage line 202
  18. lemma OAI.CompleteCrouzeix.reciprocalCorrection_circleAverage_right line 212
  19. lemma OAI.CompleteCrouzeix.reciprocalCorrection_circleAverage_left line 223
  20. lemma OAI.CompleteCrouzeix.dslope_id_mul line 234
  21. lemma OAI.CompleteCrouzeix.reciprocalCorrection_eq_logDeriv line 247
  22. theorem OAI.CompleteCrouzeix.exteriorCorrection_eq_reciprocal line 258
  23. theorem OAI.CompleteCrouzeix.continuousOn_of_analytic_left_offDiagonal line 288
  24. theorem OAI.CompleteCrouzeix.exteriorCorrection_continuousOn line 369
  25. def OAI.CompleteCrouzeix.exteriorMarkovKernel line 394
  26. lemma OAI.CompleteCrouzeix.two_re_circle_div line 397
  27. lemma OAI.CompleteCrouzeix.re_div_eq_support line 408
  28. theorem OAI.CompleteCrouzeix.exteriorMarkovKernel_nonneg line 413