OAI/NumberTheory/Catalan/Arithmetic/OddPrimePlusStartingDigits.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.centralCoeff_half_prime_reduced_residue line 8
  2. theorem OAI.InternalCatalan.boundaryFactor_odd_multiple_reduction line 21
  3. theorem OAI.InternalCatalan.boundaryFactor_odd_even_digit_reduction line 109
  4. theorem OAI.InternalCatalan.boundaryFactor_odd_even_remainder_reduction line 180
  5. theorem OAI.InternalCatalan.boundaryFactor_small_valuation_zero line 210
  6. theorem OAI.InternalCatalan.boundaryPlusWeight_small_den_ne_zero line 222
  7. theorem OAI.InternalCatalan.boundaryPlusWeight_even_nonmultiple_reduction line 238
  8. theorem OAI.InternalCatalan.boundaryPlusWeight_odd_nonmultiple_reduction line 262
  9. theorem OAI.InternalCatalan.two_div_square_mul_residue line 283
  10. theorem OAI.InternalCatalan.boundaryPlusWeight_even_multiple_reduction line 310
  11. theorem OAI.InternalCatalan.boundaryPlusWeight_odd_multiple_reduction line 350
  12. def OAI.InternalCatalan.momentScalarPred line 402
  13. theorem OAI.InternalCatalan.momentScalarPred_zero line 405
  14. theorem OAI.InternalCatalan.momentScalarPred_of_odd line 408
  15. theorem OAI.InternalCatalan.momentScalarPred_of_even line 417
  16. theorem OAI.InternalCatalan.momentScalarPred_small_valuation_nonneg line 424
  17. theorem OAI.InternalCatalan.momentScalarPred_scaled_valuation_nonneg line 432
  18. theorem OAI.InternalCatalan.momentScalarPred_prime_digit_reduction line 447
  19. theorem OAI.InternalCatalan.boundaryMinus_odd_explicit line 531
  20. theorem OAI.InternalCatalan.boundaryMinus_odd_scaled_product line 543
  21. theorem OAI.InternalCatalan.boundaryMinus_odd_digit_reduction line 549
  22. def OAI.InternalCatalan.boundaryPlusParitySum line 620
  23. theorem OAI.InternalCatalan.boundaryPlusParitySum_zero line 623
  24. theorem OAI.InternalCatalan.boundaryPlusParitySum_succ line 626
  25. theorem OAI.InternalCatalan.boundaryPlusParitySum_eq line 631
  26. theorem OAI.InternalCatalan.boundaryPlusParitySum_small_den_ne_zero line 634
  27. theorem OAI.InternalCatalan.plusParityTerm_scaled_nonmultiple line 646
  28. theorem OAI.InternalCatalan.plusParityTerm_scaled_multiple line 662
  29. theorem OAI.InternalCatalan.boundaryPlusParitySum_prime_digit_reduction line 700
  30. theorem OAI.InternalCatalan.plus_start_small_H_den line 751
  31. theorem OAI.InternalCatalan.boundaryPlus_small_successor_den_ne_zero line 763
  32. theorem OAI.InternalCatalan.boundaryPlus_prime_digit_reduction line 769