OAI/NumberTheory/Catalan/Estimates/MixedOneStart.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.hasDerivAt_sqrt_one_sub_sq line 14
  2. theorem OAI.InternalCatalan.mixedOne_complement_cancel line 22
  3. theorem OAI.InternalCatalan.integral_mixedOne_logKernel line 37
  4. theorem OAI.InternalCatalan.mixed_affine_denominator_pos line 80
  5. theorem OAI.InternalCatalan.integral_reciprocal_affine line 88
  6. theorem OAI.InternalCatalan.intervalIntegrable_mixedMoment_outer line 106
  7. theorem OAI.InternalCatalan.integral_mixedZeroLogKernel line 118
  8. theorem OAI.InternalCatalan.mixedMoment_zero_zero_eq_log_integral line 179
  9. theorem OAI.InternalCatalan.mixedMoment_zero_zero line 220
  10. theorem OAI.InternalCatalan.integral_s_reciprocal_affine line 226
  11. theorem OAI.InternalCatalan.mixedMoment_zero_one_eq_log_integral line 251
  12. theorem OAI.InternalCatalan.mixedMoment_zero_one line 297