OAI/NumberTheory/Catalan/Arithmetic/OddPrimeLowerMomentDigits.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.boundaryFactor_even_multiple_reciprocal_reduction line 9
  2. theorem OAI.InternalCatalan.boundaryFactor_even_reciprocal_valuation_nonneg line 72
  3. theorem OAI.InternalCatalan.boundaryFactor_even_reciprocal_den_ne_zero line 84
  4. theorem OAI.InternalCatalan.boundaryFactor_reciprocal_down_step line 90
  5. theorem OAI.InternalCatalan.evenBlock_cast_sub line 99
  6. theorem OAI.InternalCatalan.boundaryFactor_even_block_reciprocal_reduction line 105
  7. theorem OAI.InternalCatalan.boundaryMinusWeight_even_scaled_eq line 194
  8. theorem OAI.InternalCatalan.boundaryMinusWeight_even_block_sum_reduction line 200
  9. theorem OAI.InternalCatalan.lowerStrip_pred_succ line 286
  10. theorem OAI.InternalCatalan.momentLowerStrip_term_zero line 290
  11. theorem OAI.InternalCatalan.momentLowerStrip_term_multiple line 312
  12. theorem OAI.InternalCatalan.parityBoundarySum_even_range line 379
  13. theorem OAI.InternalCatalan.boundaryMinusWeight_even_residue_block line 389
  14. theorem OAI.InternalCatalan.boundaryMinus_small_even_residue_sum line 411
  15. theorem OAI.InternalCatalan.boundaryMinus_even_digit_reduction line 441
  16. def OAI.InternalCatalan.momentLowerStrip line 534
  17. theorem OAI.InternalCatalan.momentLowerStrip_zero line 537
  18. theorem OAI.InternalCatalan.momentLowerStrip_succ line 540
  19. theorem OAI.InternalCatalan.momentRat_lower_strip line 546
  20. theorem OAI.InternalCatalan.momentLowerStrip_prime_digit_reduction line 551
  21. theorem OAI.InternalCatalan.boundaryMinus_prime_digit_reduction line 605
  22. theorem OAI.InternalCatalan.momentRat_lower_prime_digit_reduction line 618
  23. theorem OAI.InternalCatalan.momentRat_prime_digit_reduction_of_le line 645