OAI/Combinatorics/Progressions/Probability/ShiftedSmoothProductLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rectangular_profile_mass_lower line 12
  2. def OAI.Erdos3.shiftedSmoothProductMass line 40
  3. theorem OAI.Erdos3.shiftedSmoothProductMass_eq_prod line 43
  4. theorem OAI.Erdos3.shiftedSmoothProductMass_lower line 48
  5. def OAI.Erdos3.shiftedSmoothProductPMF line 59
  6. theorem OAI.Erdos3.shiftedSmoothProductPMF_toReal line 65
  7. theorem OAI.Erdos3.shiftedSmoothProductPMF_toReal_sum line 71
  8. theorem OAI.Erdos3.shiftedSmoothProductPMF_toReal_zero_off line 77