OAI/NumberTheory/Catalan/Analysis/ZetaIntegral.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.zetaTerm line 24
  2. def OAI.InternalCatalan.zetaSeries line 27
  3. theorem OAI.InternalCatalan.zetaTerm_nonneg line 29
  4. theorem OAI.InternalCatalan.zetaTerm_le_inverse_square line 33
  5. theorem OAI.InternalCatalan.summable_inverse_square_succ line 44
  6. theorem OAI.InternalCatalan.summable_zetaTerm line 53
  7. theorem OAI.InternalCatalan.summable_norm_zetaTerm line 59
  8. theorem OAI.InternalCatalan.hasSum_zetaSeries line 64
  9. theorem OAI.InternalCatalan.tendsto_partial_sums_zetaSeries line 67
  10. theorem OAI.InternalCatalan.zetaSeries_nonneg line 72
  11. theorem OAI.InternalCatalan.zetaSeries_symm line 75
  12. theorem OAI.InternalCatalan.zetaTerm_shift line 80
  13. theorem OAI.InternalCatalan.zetaSeries_split line 84
  14. theorem OAI.InternalCatalan.zetaSeries_step line 90
  15. theorem OAI.InternalCatalan.tendsto_zetaSeries_diagonal_tail line 97
  16. theorem OAI.InternalCatalan.zetaSeries_zero_zero line 102
  17. theorem OAI.InternalCatalan.zetaSeries_diagonal line 106
  18. theorem OAI.InternalCatalan.summable_odd_reciprocal_squares line 123
  19. theorem OAI.InternalCatalan.norm_catalan_summand line 132
  20. theorem OAI.InternalCatalan.summable_norm_catalan_summand line 137
  21. theorem OAI.InternalCatalan.summable_catalan_summand line 141
  22. theorem OAI.InternalCatalan.hasSum_catalan line 146
  23. theorem OAI.InternalCatalan.tendsto_partial_sums_catalan line 150
  24. theorem OAI.InternalCatalan.hasSum_zetaKernel line 164
  25. theorem OAI.InternalCatalan.integrableOn_pow_unit line 178
  26. theorem OAI.InternalCatalan.integrable_zetaMonomial line 183
  27. theorem OAI.InternalCatalan.integral_zetaMonomial line 189
  28. theorem OAI.InternalCatalan.hasSum_catalanLogKernel line 205
  29. theorem OAI.InternalCatalan.intervalIntegrable_catalanLogKernel line 217
  30. theorem OAI.InternalCatalan.integrableOn_catalanLogKernel line 226
  31. theorem OAI.InternalCatalan.integral_Ioo_catalanLogKernel line 231
  32. theorem OAI.InternalCatalan.integral_catalanLogKernel line 271
  33. theorem OAI.InternalCatalan.hasSum_reciprocal_squares_zetaSeries line 276
  34. theorem OAI.InternalCatalan.hasSum_even_reciprocal_squares line 289
  35. theorem OAI.InternalCatalan.tsum_odd_reciprocal_squares line 298
  36. theorem OAI.InternalCatalan.hasSum_oddLogKernel line 306
  37. theorem OAI.InternalCatalan.integral_Ioo_oddLogKernel line 318
  38. theorem OAI.InternalCatalan.integral_two_oddLogKernel line 352
  39. theorem OAI.InternalCatalan.ae_mem_unit_square line 373
  40. theorem OAI.InternalCatalan.integral_prod_zetaKernel line 382
  41. theorem OAI.InternalCatalan.integrable_zetaKernel line 413
  42. theorem OAI.InternalCatalan.integral_zetaKernel line 425
  43. theorem OAI.InternalCatalan.zetaMoment_X_pow line 435