OAI/NumberTheory/Catalan/Estimates/TwoAdicSmoothingDecomposition.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.centralCoeff_two_adic_eq line 12
  2. theorem OAI.InternalCatalan.centralCoeff_two_adic_lower line 27
  3. theorem OAI.InternalCatalan.odd_nat_two_adic_eq_zero line 32
  4. theorem OAI.InternalCatalan.momentScalar_even_two_adic_eq line 38
  5. theorem OAI.InternalCatalan.centralBinom_two_adic_le_log line 50
  6. theorem OAI.InternalCatalan.momentScalar_even_two_adic_lower line 59
  7. theorem OAI.InternalCatalan.momentScalar_even_div_two_adic_lower line 67
  8. def OAI.InternalCatalan.smoothingTerm line 89
  9. theorem OAI.InternalCatalan.smoothingTerm_norm_le_zpow line 92
  10. theorem OAI.InternalCatalan.smoothingTerm_norm_le line 120
  11. theorem OAI.InternalCatalan.smoothing_majorant_summable line 149
  12. theorem OAI.InternalCatalan.smoothingTerm_summable_norm line 163
  13. theorem OAI.InternalCatalan.smoothingTerm_summable line 169
  14. def OAI.InternalCatalan.smoothingMoment line 172
  15. theorem OAI.InternalCatalan.smoothingMoment_hasSum line 174
  16. theorem OAI.InternalCatalan.smoothingTerm_tendsto_zero line 178
  17. theorem OAI.InternalCatalan.smoothingMoment_step line 182
  18. theorem OAI.InternalCatalan.smoothing_square_le_pow line 204
  19. theorem OAI.InternalCatalan.smoothingTerm_norm_le_uniform line 222
  20. theorem OAI.InternalCatalan.smoothingMoment_norm_le_uniform line 256
  21. theorem OAI.InternalCatalan.smoothingScalar_step line 281
  22. theorem OAI.InternalCatalan.momentScalar_padic_tendsto_zero line 300
  23. theorem OAI.InternalCatalan.smoothing_sum_range_sub_add_two line 318
  24. theorem OAI.InternalCatalan.smoothing_hasSum_sub_add_two_value line 327
  25. theorem OAI.InternalCatalan.smoothingMoment_first_boundary_step line 338
  26. theorem OAI.InternalCatalan.smoothingMoment_one_zero line 372
  27. theorem OAI.InternalCatalan.smoothingMoment_second_boundary_step line 395
  28. theorem OAI.InternalCatalan.smoothingMoment_minus_decomposition line 446
  29. theorem OAI.InternalCatalan.smoothingMoment_plus_succ_decomposition line 476
  30. theorem OAI.InternalCatalan.smoothingMoment_decomposition line 511
  31. theorem OAI.InternalCatalan.smoothingMoment_discrepancies line 553