OAI/NumberTheory/Catalan/Analysis/CauchyLocalLogBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.imaginary_path_hasDerivAt line 15
  2. theorem OAI.InternalCatalan.cauchyLogLeftPrimitive_hasDerivAt line 21
  3. theorem OAI.InternalCatalan.cauchyLogRightPrimitive_hasDerivAt line 34
  4. theorem OAI.InternalCatalan.intervalIntegrable_cauchyConstantKernel line 48
  5. theorem OAI.InternalCatalan.integral_cauchyConstantKernel_eq_left line 56
  6. theorem OAI.InternalCatalan.integral_cauchyConstantKernel_eq_right line 66
  7. theorem OAI.InternalCatalan.log_two_mul_nat_le line 79
  8. theorem OAI.InternalCatalan.complex_log_norm_le_nat_add_pi line 87
  9. theorem OAI.InternalCatalan.intervalIntegrable_cauchyConstantKernel_interval line 104
  10. theorem OAI.InternalCatalan.cauchyConstantKernel_interval_norm_le_three_mul line 112