OAI/NumberTheory/Jacobsthal/Primes/PrimeDensityBlocks.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.dyadicPrimes line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.mem_dyadicPrimes line 18
  3. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.dyadicPrimes_subset_survivors line 23
  4. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.dyadicPrimes_card_le line 46
  5. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.self_le_two_pow line 58
  6. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.dyadic_density_sum_le line 66
  7. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.geometricPrimes line 106
  8. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.mem_geometricPrimes line 109
  9. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.dyadicPrimes_disjoint line 114
  10. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.geometricPrimes_eq_dyadic_union line 128
  11. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.geometric_reciprocal_sum_le line 155
  12. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.subset_geometric_density_sum_le line 178
  13. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.lastBlock line 186
  14. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.blockIndices line 188
  15. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.primeBlock line 190
  16. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.geometricPrimes_disjoint line 192
  17. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.primeBlock_pairwise line 206
  18. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.primeBlock_union line 211
  19. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.primeBlock_density_sum_le line 236
  20. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.reverseOrder line 241
  21. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.supportCost line 243
  22. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.supportCost_succ line 246
  23. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.supportCost_le line 262
  24. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.supportCost_le_twelve line 272
  25. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.lastBlock_lower_le line 276
  26. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.supportHeight_product_le line 282
  27. def OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.actualLowerCoefficient line 294
  28. theorem OAI.Erdos970.NumberTheoryLean.PrimeDensityBlocks.actualLowerCoefficient_support line 298