OAI/NumberTheory/Catalan/Estimates/ScalarMomentDecay.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.scalarMoment line 18
  2. theorem OAI.InternalCatalan.sine_deriv_nonneg line 21
  3. theorem OAI.InternalCatalan.scalar_sine_cancel line 28
  4. theorem OAI.InternalCatalan.scalarMoment_eq_sine line 36
  5. theorem OAI.InternalCatalan.intervalIntegrable_scalarMoment line 50
  6. theorem OAI.InternalCatalan.scalarMoment_integrand_odd line 65
  7. theorem OAI.InternalCatalan.scalarMoment_odd line 71
  8. theorem OAI.InternalCatalan.scalarMoment_eq_zero_of_odd line 79
  9. theorem OAI.InternalCatalan.interval_even_double line 83
  10. theorem OAI.InternalCatalan.scalarMoment_even_eq_sine line 99
  11. theorem OAI.InternalCatalan.two_integral_sine_odd_eq_momentScalar line 115
  12. theorem OAI.InternalCatalan.scalarMoment_eq_momentScalar line 144
  13. theorem OAI.InternalCatalan.scalarMoment_zero line 151
  14. theorem OAI.InternalCatalan.tendsto_scalarMoment_zero line 160
  15. theorem OAI.InternalCatalan.tendsto_momentScalar_zero line 198