OAI/Analysis/Crouzeix/HomologicalCauchy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Homological Cauchy.

  1. def OAI.CrouzeixHilbert.extendCompactFunction line 18
  2. theorem OAI.CrouzeixHilbert.extendCompactFunction_apply line 24
  3. def OAI.CrouzeixHilbert.holomorphicContinuousFunctions line 30
  4. theorem OAI.CrouzeixHilbert.isClosed_holomorphicContinuousFunctions line 48
  5. theorem OAI.CrouzeixHilbert.differentiableOn_parameter_intervalIntegral line 62
  6. theorem OAI.CrouzeixHilbert.dslope_swap line 120
  7. theorem OAI.CrouzeixHilbert.continuousAt_dslope_pair_of_analyticAt line 126
  8. theorem OAI.CrouzeixHilbert.continuousOn_dslope_pair line 155
  9. def OAI.CrouzeixHilbert.SmoothContour.integral line 174
  10. def OAI.CrouzeixHilbert.SmoothContour.cauchyTransform line 179
  11. def OAI.CrouzeixHilbert.SmoothContour.regularizedTransform line 183
  12. theorem OAI.CrouzeixHilbert.SmoothContour.intervalIntegrable_contourIntegrand line 187
  13. theorem OAI.CrouzeixHilbert.SmoothContour.differentiableOn_cauchyTransform line 196
  14. theorem OAI.CrouzeixHilbert.SmoothContour.differentiableOn_regularizedTransform line 220
  15. theorem OAI.CrouzeixHilbert.SmoothContour.regularizedTransform_eq line 237
  16. theorem OAI.CrouzeixHilbert.SmoothContour.eventually_index_eq line 262
  17. theorem OAI.CrouzeixHilbert.SmoothContour.tendsto_cauchyTransform_cocompact line 271
  18. theorem OAI.CrouzeixHilbert.SmoothContour.eventually_index_zero_cocompact line 313
  19. theorem OAI.CrouzeixHilbert.SmoothContour.tendsto_regularizedTransform_cocompact line 323
  20. theorem OAI.CrouzeixHilbert.sum_regularizedTransform_eq_zero line 331
  21. theorem OAI.CrouzeixHilbert.sum_integral_eq_zero_of_null_homology line 373