OAI/Combinatorics/Progressions/Lattices/StrideSelectedResidueBadProduct.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.badPrimeModulusEvent_probability line 13
  2. theorem OAI.Erdos3.badPrimeModulusEvent_probability_bounded line 31
  3. theorem OAI.Erdos3.independent_badPrime_joint_probability line 60
  4. theorem OAI.Erdos3.independent_badPrimeModulusEvent_probability line 100
  5. theorem OAI.Erdos3.largestBadPrimeProduct_probability line 127
  6. theorem OAI.Erdos3.largestBadPrimeProduct_probability_exact line 169
  7. def OAI.Erdos3.primeArrayBad line 193
  8. theorem OAI.Erdos3.primeArrayBad_iff line 197
  9. theorem OAI.Erdos3.independent_largestBadPrimeProduct_probability line 206
  10. theorem OAI.Erdos3.largestBadPrimeProduct_probability_bounded line 233
  11. theorem OAI.Erdos3.exists_early_badPrime_radius line 287
  12. theorem OAI.Erdos3.exists_early_badPrimeProduct_cutoff line 318
  13. def OAI.Erdos3.quantitativeBadPrimeRadius line 346
  14. theorem OAI.Erdos3.quantitativeBadPrimeRadius_bounds line 348
  15. theorem OAI.Erdos3.quantitativeBadPrimeRadius_error line 395
  16. theorem OAI.Erdos3.quantitativeBadPrimeRadius_witness_budget line 410
  17. def OAI.Erdos3.selectedResidueTiltedFiniteLaw line 468
  18. theorem OAI.Erdos3.selectedResidueTiltedFiniteLaw_mean line 478
  19. theorem OAI.Erdos3.selectedResidue_fiber_excess_le line 491
  20. theorem OAI.Erdos3.selectedResidueTiltedFiniteLaw_event line 526
  21. theorem OAI.Erdos3.selectedResidueDensityPMF_badPrimeProduct_probability line 534
  22. theorem OAI.Erdos3.exists_early_selectedResidueDensityPMF_badPrimeProduct_cutoff line 571
  23. def OAI.Erdos3.prescribedDeepBad line 606
  24. theorem OAI.Erdos3.largestTestedBadDepth_le_prescribed_max line 609
  25. theorem OAI.Erdos3.largestBadPrimeProduct_le_prescribed line 621
  26. theorem OAI.Erdos3.selectedResidueDensityPMF_prescribed_badPrimeProduct line 634
  27. theorem OAI.Erdos3.selected_factorization_product_dvd line 702
  28. theorem OAI.Erdos3.selected_double_factorization_product_dvd line 719
  29. theorem OAI.Erdos3.selected_double_factorization_product_le line 725
  30. theorem OAI.Erdos3.largestBadPrimeProduct_le_stride_sq line 730
  31. theorem OAI.Erdos3.crtPolynomialCharge_le_of_deep_bad_product line 740
  32. theorem OAI.Erdos3.column_stride_factorization_le_product line 756
  33. theorem OAI.Erdos3.column_stride_depth_lt_of_product_stride line 764
  34. theorem OAI.Erdos3.column_stride_depth_le_of_product_stride line 770
  35. theorem OAI.Erdos3.selectedResidueDensityPMF_stride_badPrimeProduct line 786