OAI/Combinatorics/Progressions/Lattices/SmoothBadPrimeProduct.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coefficientCRTEquiv line 14
  2. theorem OAI.Erdos3.coefficientCRTEquiv_apply line 27
  3. theorem OAI.Erdos3.coefficientCRTEquiv_intCast line 34
  4. theorem OAI.Erdos3.uniform_map_equiv line 41
  5. theorem OAI.Erdos3.dependentProductPMF_uniform line 49
  6. theorem OAI.Erdos3.uniform_coefficientCRT_map line 59
  7. theorem OAI.Erdos3.selectedPrimePower_coprime line 67
  8. theorem OAI.Erdos3.selectedPrimePower_nonzero line 74
  9. theorem OAI.Erdos3.uniform_selectedPrimePowerCRT_map line 80
  10. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_residue_apply line 102
  11. theorem OAI.Erdos3.shiftedSmoothSampleSum_sub_width_abs_le line 134
  12. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_residue_error line 146
  13. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_residue_l1 line 185
  14. def OAI.Erdos3.smoothCoefficientResidueWeights line 206
  15. theorem OAI.Erdos3.smoothCoefficientProduct_residue_event_error line 211
  16. theorem OAI.Erdos3.smoothCoefficientProduct_residue_event_error_of_width line 236
  17. theorem OAI.Erdos3.shiftedSmoothProductPMF_residue_weight line 258
  18. theorem OAI.Erdos3.shiftedSmoothProductPMF_residue_event_error line 271
  19. theorem OAI.Erdos3.shiftedSmoothProductPMF_residue_l1 line 284
  20. theorem OAI.Erdos3.shiftedSmoothProductPMF_residue_complexMean_error line 304
  21. theorem OAI.Erdos3.shiftedSmoothProductPMF_residue_transfer line 316
  22. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_residue_complexMean_error line 342
  23. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_residue_event_error line 356
  24. theorem OAI.Erdos3.residue_error_sum_le_of_width line 370
  25. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_residue_complexMean_error_of_width line 385
  26. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_residue_event_error_of_width line 404
  27. theorem OAI.Erdos3.uniform_coefficientCRT_event line 433
  28. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_primePower_event line 461
  29. def OAI.Erdos3.smoothResiduePrimeBad line 510
  30. theorem OAI.Erdos3.smoothResidue_badPrimeProduct_probability line 515
  31. theorem OAI.Erdos3.exists_early_smoothResidue_badPrimeProduct_cutoff line 570