OAI/Analysis/DirectCrouzeix/CompactIntegrals.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Faber.integrable_of_continuous_compact line 19
  2. theorem OAI.DirectCrouzeix.Faber.continuousOn_integral_compact line 25
  3. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_integral_compact line 46
  4. abbrev OAI.DirectCrouzeix.Faber.Parameter line 73
  5. def OAI.DirectCrouzeix.Faber.chord line 75
  6. theorem OAI.DirectCrouzeix.Faber.chord_mem line 77
  7. theorem OAI.DirectCrouzeix.Faber.continuous_chord line 81
  8. def OAI.DirectCrouzeix.Faber.chordIntegral line 85
  9. theorem OAI.DirectCrouzeix.Faber.continuousOn_chordIntegral line 88
  10. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_chord_left line 99
  11. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_chord_right line 103
  12. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_chordIntegral_left line 107
  13. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_chordIntegral_right line 127
  14. theorem OAI.DirectCrouzeix.Faber.chordIntegral_one_eq_interval line 147
  15. theorem OAI.DirectCrouzeix.Faber.hasDerivAt_chord_time line 154
  16. theorem OAI.DirectCrouzeix.Faber.chordIntegral_deriv_mul line 162
  17. theorem OAI.DirectCrouzeix.Faber.chordIntegral_deriv_eq_dslope line 179
  18. theorem OAI.DirectCrouzeix.Faber.analyticOnNhd_chordIntegral_left line 193
  19. theorem OAI.DirectCrouzeix.Faber.analyticOnNhd_chordIntegral_right line 200