OAI/Combinatorics/Progressions/Probability/PMFPointMassMixture.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.pmf_toReal_hasSum line 13
  2. theorem OAI.Erdos3.pmf_complex_average_summable line 21
  3. theorem OAI.Erdos3.pmf_complex_average_error line 29
  4. theorem OAI.Erdos3.pmf_bind_toReal line 44
  5. theorem OAI.Erdos3.pmf_bind_scaled_complex_average line 50
  6. theorem OAI.Erdos3.pmf_bind_point_error line 60
  7. theorem OAI.Erdos3.pmf_bind_measure_eq_sum line 96
  8. theorem OAI.Erdos3.pmf_bind_integral_tsum line 105
  9. theorem OAI.Erdos3.pmf_integral_bind line 114
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.integral_bind_real line 124
  11. theorem OAI.Erdos3.pmf_bind_toReal_integral line 145
  12. theorem OAI.Erdos3.pmf_bind_point_approximation_error line 157