OAI/Combinatorics/Progressions/Lattices/ResiduePrimeDensityError.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_prime_coordinate_integer_anchor line 15
  2. theorem OAI.Erdos3.primeCoordinateCell_eq_integer_anchor line 49
  3. def OAI.Erdos3.primeCoordinateMassRatio line 74
  4. theorem OAI.Erdos3.primeCoordinate_weighted_fiber line 80
  5. theorem OAI.Erdos3.primeCoordinateDensity_conditional line 111
  6. theorem OAI.Erdos3.primeCoordinateReference_fiber line 124
  7. theorem OAI.Erdos3.primeCoordinateMassRatio_eq_count line 135
  8. theorem OAI.Erdos3.primeCoordinateDensity_conditional_one line 144
  9. theorem OAI.Erdos3.primeCoordinateCell_card_residue line 168
  10. theorem OAI.Erdos3.primeCoordinateMassRatio_close line 180
  11. theorem OAI.Erdos3.primeCoordinateDensity_productMarginalsClose line 214
  12. def OAI.Erdos3.residuePrimeCoordinateLaw line 236
  13. def OAI.Erdos3.residuePrimeCoordinateDensity line 245
  14. def OAI.Erdos3.residuePrimeCoordinateMassRatio line 255
  15. theorem OAI.Erdos3.residuePrimeCoordinateDensity_conditional line 262
  16. theorem OAI.Erdos3.residuePrimeCoordinateMassRatio_eq_count line 278
  17. theorem OAI.Erdos3.residuePrimeCoordinateDensity_conditional_one line 288
  18. theorem OAI.Erdos3.residuePrimeCoordinateDensity_one line 305
  19. theorem OAI.Erdos3.primeCoordinateMean_re line 323
  20. theorem OAI.Erdos3.primeCoordinateRealMean_bound line 329
  21. theorem OAI.Erdos3.primeCoordinateDensity_conditional_error line 346
  22. theorem OAI.Erdos3.primeCoordinateDensity_sectionMarginalsClose line 362
  23. def OAI.Erdos3.normalizedResiduePrimeDensity line 387
  24. theorem OAI.Erdos3.normalizedResiduePrimeDensity_low_degree line 394
  25. theorem OAI.Erdos3.residuePrimeCoordinateMassRatio_close_of_marginals line 439
  26. theorem OAI.Erdos3.residuePrimeCoordinateCell_nonempty_of_marginals line 448
  27. theorem OAI.Erdos3.residuePrimeCoordinateMassRatio_affine line 471
  28. theorem OAI.Erdos3.residuePrimeCoordinateMassRatio_close line 485
  29. theorem OAI.Erdos3.residuePrimeCoordinateCell_nonempty_of_small line 506
  30. theorem OAI.Erdos3.residuePrimeCoordinateDensity_productMarginalsClose line 523
  31. theorem OAI.Erdos3.residuePrimeCoordinateDensity_sectionMarginalsClose line 539
  32. theorem OAI.Erdos3.residuePrimeCoordinateMean_re line 567
  33. theorem OAI.Erdos3.residuePrimeCoordinateRealMean_bound line 576
  34. theorem OAI.Erdos3.residuePrimeCoordinateDensity_conditional_error line 596