OAI/Combinatorics/Progressions/Sampling/SmoothSplitSampling.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.smoothSampleSum line 13
  2. theorem OAI.Erdos3.smoothProfileSamples_summable line 16
  3. theorem OAI.Erdos3.smoothSampleSum_pos line 24
  4. theorem OAI.Erdos3.smoothSampleSum_error line 30
  5. def OAI.Erdos3.smoothCoefficientPMF line 39
  6. theorem OAI.Erdos3.smoothCoefficientPMF_apply line 44
  7. theorem OAI.Erdos3.smoothProductSamples_summable line 58
  8. theorem OAI.Erdos3.smoothProductSamples_sum line 67
  9. theorem OAI.Erdos3.smoothProductSamples_sum_pos line 88
  10. def OAI.Erdos3.smoothProductPMF line 94
  11. theorem OAI.Erdos3.smoothProductPMF_apply line 100
  12. def OAI.Erdos3.shiftedSmoothSampleSum line 117
  13. theorem OAI.Erdos3.shiftedSmoothSamples_summable line 120
  14. theorem OAI.Erdos3.shiftedSmoothSampleSum_error line 125
  15. theorem OAI.Erdos3.shiftedSmoothSampleSum_pos line 133
  16. def OAI.Erdos3.shiftedSmoothCoefficientPMF line 146
  17. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_apply line 151
  18. theorem OAI.Erdos3.shiftedSmoothProductSamples_sum line 157
  19. theorem OAI.Erdos3.scaledInputWeightSum_splitSmoothProductProfile line 187
  20. theorem OAI.Erdos3.scaledInputMass_splitSmoothProductProfile_pos line 198
  21. theorem OAI.Erdos3.scaledInputPMF_splitSmoothProductProfile line 208
  22. theorem OAI.Erdos3.splitInputProfile_smooth line 232
  23. theorem OAI.Erdos3.smoothSplit_weight_sum line 241
  24. theorem OAI.Erdos3.smoothSplit_mass_pos line 255
  25. theorem OAI.Erdos3.smoothSplit_mass_product line 264
  26. theorem OAI.Erdos3.smoothSplit_inputPMF_apply line 271