OAI/NumberTheory/Jacobsthal/Primes/PrimeEventCounting.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_residue_fibre_bound line 18
  2. def OAI.Erdos970.ErdosVarianceSmallModel.goodPrimes line 85
  3. def OAI.Erdos970.ErdosVarianceSmallModel.primeM line 87
  4. def OAI.Erdos970.ErdosVarianceSmallModel.primeK line 92
  5. def OAI.Erdos970.ErdosVarianceSmallModel.primePoint line 97
  6. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeMK_identity line 105
  7. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeM_bounds line 111
  8. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeM_coprime line 118
  9. theorem OAI.Erdos970.ErdosVarianceSmallModel.primePoint_mem_model line 133
  10. def OAI.Erdos970.ErdosVarianceSmallModel.primeFibre line 154
  11. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeFibre_image_subset line 159
  12. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeFibre_card_le_residue line 183
  13. def OAI.Erdos970.ErdosVarianceSmallModel.indexedPrimeEvent line 204
  14. def OAI.Erdos970.ErdosVarianceSmallModel.actualPrimeEvent line 209
  15. theorem OAI.Erdos970.ErdosVarianceSmallModel.actualPrimeEvent_card line 214
  16. theorem OAI.Erdos970.ErdosVarianceSmallModel.actualPrimeEvent_card_fibres line 220