OAI/Analysis/DirectCrouzeix/DividedDifferences.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Faber.divided line 17
  2. def OAI.DirectCrouzeix.Faber.dividedLeft line 19
  3. def OAI.DirectCrouzeix.Faber.chordDenominator line 22
  4. def OAI.DirectCrouzeix.Faber.correction line 24
  5. theorem OAI.DirectCrouzeix.Faber.divided_eq_dslope line 27
  6. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_divided_left line 31
  7. theorem OAI.DirectCrouzeix.Faber.continuousOn_correction line 37
  8. theorem OAI.DirectCrouzeix.Faber.analyticOnNhd_correction_left line 49
  9. theorem OAI.DirectCrouzeix.Faber.analyticOnNhd_correction_right line 60
  10. theorem OAI.DirectCrouzeix.Faber.correction_zero_left line 71
  11. theorem OAI.DirectCrouzeix.Faber.correction_zero_right line 74
  12. def OAI.DirectCrouzeix.Faber.exterior line 77
  13. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_exterior line 79
  14. theorem OAI.DirectCrouzeix.Faber.chordDenominator_off_diagonal line 88
  15. theorem OAI.DirectCrouzeix.Faber.chordDenominator_diagonal line 97
  16. theorem OAI.DirectCrouzeix.Faber.chordDenominator_ne_zero line 103
  17. theorem OAI.DirectCrouzeix.Faber.divided_fundamental line 123
  18. theorem OAI.DirectCrouzeix.Faber.divided_derivative_relation line 130
  19. theorem OAI.DirectCrouzeix.Faber.correction_identity line 140