OAI/NumberTheory/PrimeGaps/EulerProducts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.fiberSubsetFamily line 21
  2. theorem OAI.LargePrimeGaps.mem_fiberSubsetFamily line 26
  3. theorem OAI.LargePrimeGaps.disjoint_nonemptySubsets_fibers line 37
  4. theorem OAI.LargePrimeGaps.fiberSubsetFamily_sign_sum line 49
  5. theorem OAI.LargePrimeGaps.mem_fiberSubsetFamily_image line 63
  6. theorem OAI.LargePrimeGaps.eulerP_zero_fiber_family line 76
  7. theorem OAI.LargePrimeGaps.eulerH_zero_fiber_families line 85
  8. def OAI.LargePrimeGaps.shiftFamily line 95
  9. def OAI.LargePrimeGaps.residueFamily line 98
  10. def OAI.LargePrimeGaps.markedResidueFamily line 101
  11. theorem OAI.LargePrimeGaps.mem_markedResidueFamily line 104
  12. theorem OAI.LargePrimeGaps.residueFamily_eq_shiftFamily line 117
  13. theorem OAI.LargePrimeGaps.markedResidueFamily_eq_shiftFamily line 130
  14. theorem OAI.LargePrimeGaps.one_sub_prime_inv_ne_zero line 141
  15. theorem OAI.LargePrimeGaps.eulerH_unmarked_zero line 149
  16. theorem OAI.LargePrimeGaps.residueCount_insert_eq line 162
  17. theorem OAI.LargePrimeGaps.eulerH_marked_zero line 170
  18. theorem OAI.LargePrimeGaps.multipliable_of_summable_norm_sub_one line 196
  19. theorem OAI.LargePrimeGaps.norm_tprod_sub_one_le_exp line 200
  20. theorem OAI.LargePrimeGaps.tprod_eq_prod_mul_tail line 211
  21. theorem OAI.LargePrimeGaps.norm_tprod_sub_prod_le line 221
  22. theorem OAI.LargePrimeGaps.norm_tprod_sub_tprod_le line 229
  23. theorem OAI.LargePrimeGaps.sum_reciprocal_sq_injective_le line 263
  24. theorem OAI.LargePrimeGaps.summable_tsum_le_of_reciprocal_sq line 273
  25. theorem OAI.LargePrimeGaps.norm_euler_tail_sub_one_le line 287