OAI/Combinatorics/Progressions/Probability/ShiftedProductCoordinateLaw.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coefficientWeight line 11
  2. def OAI.Erdos3.coefficientWeightSum line 14
  3. theorem OAI.Erdos3.coefficientWeight_summable line 17
  4. def OAI.Erdos3.coefficientPMF line 27
  5. def OAI.Erdos3.coefficientImagePMF line 34
  6. theorem OAI.Erdos3.selectedCoefficientEquiv_normalize line 40
  7. def OAI.Erdos3.selectedIntegerCoefficientEquiv line 50
  8. theorem OAI.Erdos3.selectedIntegerCoefficient_weight line 54
  9. theorem OAI.Erdos3.selectedCoefficient_weight_sum line 62
  10. theorem OAI.Erdos3.selectedCoefficient_weight_sum_pos line 70
  11. theorem OAI.Erdos3.dependentProductPMF_toMeasure line 85
  12. theorem OAI.Erdos3.dependentProductPMF_image_law line 91
  13. theorem OAI.Erdos3.jointCoefficientImage_law line 103
  14. theorem OAI.Erdos3.coefficientPMF_apply line 122
  15. theorem OAI.Erdos3.selectedCoefficient_input_law line 129
  16. theorem OAI.Erdos3.selectedIntegerCoefficient_mulVec line 145
  17. theorem OAI.Erdos3.selectedCoefficient_image_law line 160
  18. def OAI.Erdos3.spatialCoordinateArrayEquiv line 186
  19. theorem OAI.Erdos3.shiftedSmoothProductMass_grouped line 192
  20. theorem OAI.Erdos3.shiftedSmoothProductMass_slice_pos line 201
  21. theorem OAI.Erdos3.shiftedSmoothProductPMF_grouped line 208
  22. theorem OAI.Erdos3.shiftedSmoothProductPMF_grouped_expectation line 228
  23. theorem OAI.Erdos3.dependentProductPMF_map_of_image_law line 240