OAI/Combinatorics/Progressions/Lattices/PrimeCoordinateCells.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.periodPrimeCoordinates line 17
  2. theorem OAI.Erdos3.mem_periodPrimeCoordinates line 22
  3. theorem OAI.Erdos3.periodPrimeCoordinates_card_pow_le line 28
  4. theorem OAI.Erdos3.periodPrimeCoordinates_card_log_le line 46
  5. theorem OAI.Erdos3.periodPrimeCoordinates_card_le line 54
  6. theorem OAI.Erdos3.periodPrimeCoordinates_pending_coprime line 67
  7. theorem OAI.Erdos3.periodPrimeCoordinates_pending_mul_coprime line 79
  8. theorem OAI.Erdos3.disjoint_prime_power_products_coprime line 86
  9. theorem OAI.Erdos3.periodPrimeCoordinates_unfixed_coprime line 101
  10. theorem OAI.Erdos3.selectedPrimePowers_pairwise_coprime line 121
  11. theorem OAI.Erdos3.modEq_selected_prod_iff line 130
  12. theorem OAI.Erdos3.periodPrimeCoordinates_modulus_dvd_product line 159
  13. theorem OAI.Erdos3.periodPrimeCoordinates_card_le_of_le_pow line 170
  14. theorem OAI.Erdos3.initialResiduePrimeMask_bounds line 187
  15. theorem OAI.Erdos3.initialResidueCombined_coprime line 223
  16. def OAI.Erdos3.affineComparisonPrimeThreshold line 250
  17. def OAI.Erdos3.affineComparisonContraction line 253
  18. theorem OAI.Erdos3.affineComparisonContraction_bounds line 256
  19. def OAI.Erdos3.affineMandatoryPrimes line 289
  20. theorem OAI.Erdos3.mem_affineMandatoryPrimes line 293
  21. theorem OAI.Erdos3.affineMandatoryPrimes_outside_inverse line 298
  22. theorem OAI.Erdos3.affineMandatoryPrimes_card_le line 310
  23. def OAI.Erdos3.affineInitialPrimeMask line 342
  24. theorem OAI.Erdos3.affineInitialPrimeMask_contains line 347
  25. theorem OAI.Erdos3.affineInitialPrimeMask_card_le line 355
  26. theorem OAI.Erdos3.affineInitialPrimeMask_outside_coprime line 375
  27. def OAI.Erdos3.affineSamplerPrimeMask line 400
  28. theorem OAI.Erdos3.affineSamplerPrimeMask_contains line 404
  29. theorem OAI.Erdos3.affineSamplerPrimeMask_card_le line 411
  30. theorem OAI.Erdos3.affineSamplerPrimeMask_outside line 427
  31. def OAI.Erdos3.affineReferencePower line 453
  32. def OAI.Erdos3.affineReferenceInput line 456
  33. theorem OAI.Erdos3.affineReferenceInput_bounds line 460
  34. theorem OAI.Erdos3.affineReferenceInput_le_envelope line 470
  35. theorem OAI.Erdos3.affineReferenceInput_mask_and_depth line 489
  36. def OAI.Erdos3.primeCoordinateCell line 529
  37. theorem OAI.Erdos3.mem_primeCoordinateCell line 535
  38. theorem OAI.Erdos3.primeCoordinateCell_anchor line 542
  39. theorem OAI.Erdos3.mem_primeCoordinateCell_anchor line 554
  40. def OAI.Erdos3.primeCoordinateCellEquiv line 574
  41. theorem OAI.Erdos3.primeCoordinateCell_mean line 588