OAI/Combinatorics/Progressions/Estimates/FiniteDependentPMFBind.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.pmf_bind_pair_apply line 12
  2. theorem OAI.Erdos3.dependentProductPMF_pair line 24
  3. def OAI.Erdos3.FiniteProbabilityWeights.prod line 63
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_prod line 70
  5. def OAI.Erdos3.FiniteProbabilityWeights.toPMF line 87
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_apply line 91
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_toReal line 94
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_bind_apply line 98
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_bind_toReal line 104
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_pi line 111
  11. def OAI.Erdos3.FiniteProbabilityWeights.ofPMF line 129
  12. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPMF_weight line 137
  13. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_uniform_weight line 140
  14. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_prod line 154
  15. theorem OAI.Erdos3.FiniteProbabilityWeights.positiveWeights_pi_total line 173
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_pi line 178
  17. theorem OAI.Erdos3.FiniteProbabilityWeights.positiveWeights_prod_total line 191
  18. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_prod line 196
  19. def OAI.Erdos3.FiniteProbabilityWeights.ofSupportedPMF line 221
  20. theorem OAI.Erdos3.FiniteProbabilityWeights.ofSupportedPMF_weight line 232
  21. theorem OAI.Erdos3.FiniteProbabilityWeights.ofSupportedPMF_map_mean line 236
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.ofSupportedPMF_map_complexMean line 253
  23. theorem OAI.Erdos3.FiniteProbabilityWeights.ofSupportedPMF_map_event line 264
  24. def OAI.Erdos3.shiftedSmoothProductFiniteWeights line 273
  25. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_weight line 279
  26. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_map_event line 285
  27. theorem OAI.Erdos3.shiftedSmoothProductFiniteWeights_map_complexMean line 292
  28. theorem OAI.Erdos3.dependentProductPMF_bind_finite line 310
  29. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_prod_point_mass line 320