OAI/NumberTheory/Catalan/Arithmetic/OddPrimeOddBoundaryValuation.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.factorial_valuation_below_prime_sq line 11
2. theorem OAI.InternalCatalan.centralBinom_valuation_floor line 18
3. theorem OAI.InternalCatalan.centralBinom_valuation_single_carry line 32
4. theorem OAI.InternalCatalan.centralBinom_valuation_le_one line 42
5. theorem OAI.InternalCatalan.centralCoeff_odd_prime_valuation line 47
6. theorem OAI.InternalCatalan.centralCoeff_odd_prime_single_carry line 65
7. theorem OAI.InternalCatalan.centralCoeff_odd_prime_nonneg line 72
8. theorem OAI.InternalCatalan.nat_valuation_below_prime_sq line 77
9. theorem OAI.InternalCatalan.double_carry_iff_remainder_odd line 90
10. theorem OAI.InternalCatalan.boundaryFactor_even_odd_prime_valuation line 102
11. theorem OAI.InternalCatalan.boundaryFactor_even_odd_prime_eq_zero line 114
12. theorem OAI.InternalCatalan.boundaryFactor_even_odd_prime_eq_one line 120
13. theorem OAI.InternalCatalan.boundaryFactor_even_odd_prime_valuation_of_lt_H line 125
14. theorem OAI.InternalCatalan.boundaryFactor_even_mul_odd_prime_valuation line 131
15. theorem OAI.InternalCatalan.harmonicRat_strictMono line 149
16. theorem OAI.InternalCatalan.harmonicRat_sub_ne_zero line 155
17. theorem OAI.InternalCatalan.zetaRat_ne_zero_of_ne line 161
18. theorem OAI.InternalCatalan.harmonic_sum_prime_valuation_lower line 169
19. theorem OAI.InternalCatalan.harmonicRat_prime_sq_lower line 185
20. theorem OAI.InternalCatalan.nat_sub_not_dvd_of_mod_ne line 201
21. theorem OAI.InternalCatalan.sub_natCast_valuation_of_mod_ne line 209
22. theorem OAI.InternalCatalan.zetaRat_distinct_residue_valuation_lower line 222
23. theorem OAI.InternalCatalan.zetaRat_distinct_residue_scaled_valuation line 244
24. theorem OAI.InternalCatalan.rational_residue_zero_of_positive_valuation line 255
25. theorem OAI.InternalCatalan.zetaRat_distinct_residue_reduction line 276
26. theorem OAI.InternalCatalan.prime_sum_valuation_lower line 293
27. theorem OAI.InternalCatalan.prime_sub_valuation_lower line 308
28. theorem OAI.InternalCatalan.prime_mul_valuation_lower line 319
29. theorem OAI.InternalCatalan.prime_div_nat_valuation_lower line 330
30. theorem OAI.InternalCatalan.centralBinom_prime_valuation_le_log line 347
31. theorem OAI.InternalCatalan.centralCoeff_odd_prime_log_bounds line 355
32. theorem OAI.InternalCatalan.harmonicRat_prime_digit_error line 373
33. theorem OAI.InternalCatalan.finite_sum_valuation_zero_or_one_le line 410
34. theorem OAI.InternalCatalan.harmonicRat_prime_digit_error_valuation line 430
35. theorem OAI.InternalCatalan.two_odd_prime_valuation line 455
36. theorem OAI.InternalCatalan.boundaryFactor_odd_prime_log_bounds line 462
37. theorem OAI.InternalCatalan.momentScalar_odd_prime_log_lower line 480
38. theorem OAI.InternalCatalan.boundaryPlusWeight_odd_prime_log_lower line 498
39. theorem OAI.InternalCatalan.boundaryMinusWeight_odd_prime_log_lower line 512
40. theorem OAI.InternalCatalan.harmonicRat_prime_log_lower line 537
41. theorem OAI.InternalCatalan.zetaRat_prime_log_lower_of_le line 553
42. theorem OAI.InternalCatalan.zetaRat_prime_log_lower line 586
43. theorem OAI.InternalCatalan.prime_sub_valuation_nonneg line 599
44. theorem OAI.InternalCatalan.prime_sub_valuation_pos_or_zero line 609
45. theorem OAI.InternalCatalan.rational_den_ne_zero_of_valuation_nonneg line 624
46. theorem OAI.InternalCatalan.zero_residue_of_zero_or_positive line 636
47. theorem OAI.InternalCatalan.rational_residue_eq_of_difference line 643
48. theorem OAI.InternalCatalan.zetaRat_prime_sq_lower_of_le line 660
49. theorem OAI.InternalCatalan.zetaRat_prime_sq_scaled_valuation_nonneg line 685
50. theorem OAI.InternalCatalan.quotients_ne_of_residue_eq line 701
51. theorem OAI.InternalCatalan.sub_eq_prime_mul_quotient_sub line 709
52. theorem OAI.InternalCatalan.zetaRat_same_residue_error_identity line 720
53. theorem OAI.InternalCatalan.zetaRat_same_residue_error_valuation line 734
54. theorem OAI.InternalCatalan.zetaRat_same_residue_reduction line 776
55. theorem OAI.InternalCatalan.zetaRat_prime_digit_reduction line 802
56. theorem OAI.InternalCatalan.boundaryFactor_odd_prime_valuation line 822
57. theorem OAI.InternalCatalan.boundaryFactor_odd_inverse_valuation_nonneg line 850
58. theorem OAI.InternalCatalan.boundaryFactor_odd_scaled_valuation_nonneg line 857
59. theorem OAI.InternalCatalan.boundaryFactor_odd_integral_denominators line 866
60. theorem OAI.InternalCatalan.boundaryFactor_odd_odd_remainder_reduction line 875