OAI/NumberTheory/Catalan/Arithmetic/OddPrimeLossNormalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.oddPrimeLoss_weighted_0_25 line 19
  2. theorem OAI.InternalCatalan.oddPrimeLoss_weighted_tendsto_real line 36
  3. theorem OAI.InternalCatalan.oddPrimeLoss_prime_sum_tendsto line 54
  4. def OAI.InternalCatalan.removedPrimeLoss line 78
  5. theorem OAI.InternalCatalan.removedPrimeLoss_nonneg line 83
  6. theorem OAI.InternalCatalan.removedPrimeLoss_le line 91
  7. theorem OAI.InternalCatalan.sqrt_H_div_tendsto_zero line 131
  8. theorem OAI.InternalCatalan.removedPrimeLoss_tendsto_zero line 141
  9. theorem OAI.InternalCatalan.oddPrimeLoss_large_prime_sum_tendsto line 147
  10. theorem OAI.InternalCatalan.large_prime_cutoff_ne_two line 173
  11. theorem OAI.InternalCatalan.large_prime_cutoff_square line 192
  12. theorem OAI.InternalCatalan.large_prime_cutoff_gt_fixed line 200
  13. theorem OAI.InternalCatalan.large_prime_witness_den_eventually line 210
  14. theorem OAI.InternalCatalan.oddPrimeLoss_large_prime_normalized_tendsto line 230
  15. theorem OAI.InternalCatalan.oddPrimeLoss_large_prime_normalized_eventually_upper line 246