OAI/Analysis/Cotype/FiniteContour.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteContour.resolvent line 13
  2. def OAI.FiniteContour.laplace line 17
  3. theorem OAI.FiniteContour.resolvent_differentiableAt line 21
  4. theorem OAI.FiniteContour.scalar_cauchy line 32
  5. theorem OAI.FiniteContour.finite_cauchy line 40
  6. def OAI.FiniteContour.logKernel line 62
  7. theorem OAI.FiniteContour.logKernel_differentiableAt line 66
  8. theorem OAI.FiniteContour.log_rectangle line 74
  9. theorem OAI.FiniteContour.vertical_mul_re_lower line 90
  10. theorem OAI.FiniteContour.exponential_decay line 105
  11. theorem OAI.FiniteContour.weighted_resolvent_bound line 112
  12. theorem OAI.FiniteContour.upper_arc_sector line 124
  13. theorem OAI.FiniteContour.left_arc_sector line 138
  14. theorem OAI.FiniteContour.exp_sector line 149
  15. theorem OAI.FiniteContour.sector_ne_nonneg line 159
  16. theorem OAI.FiniteContour.angle_exists line 166
  17. theorem OAI.FiniteContour.fixed_arc_exp_bound line 177
  18. theorem OAI.FiniteContour.logKernel_circle line 189
  19. theorem OAI.FiniteContour.logKernel_ray_bound line 203
  20. theorem OAI.FiniteContour.logKernel_fixed_arc_bound line 229
  21. theorem OAI.FiniteContour.ray_integral_bound line 242
  22. theorem OAI.FiniteContour.resolvent_radius_bound line 253
  23. theorem OAI.FiniteContour.logKernel_outer_bound line 273
  24. theorem OAI.FiniteContour.logKernel_horizontal_continuous line 296
  25. theorem OAI.FiniteContour.finite_truncated_contour line 313
  26. theorem OAI.FiniteContour.norm_five line 348
  27. theorem OAI.FiniteContour.outer_tail_tendsto_zero line 356
  28. theorem OAI.finiteLaplaceSum_vertical_bound_of_sector_resolvent line 364