OAI/Probability/ThreeStateClauses/CountableStatistics.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Countable Statistics.

  1. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_measure_sum_dirac line 20
  2. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_integrable_iff line 25
  3. lemma OAI.ThreeState.TreeClauses.Experiment.integral_pmf_tsum line 30
  4. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_integrable_bind line 36
  5. lemma OAI.ThreeState.TreeClauses.Experiment.integral_pmf_bind_integrable line 47
  6. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_integrable_bind_finite line 55
  7. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_integrable_map_iff line 60
  8. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_integrable_of_square line 66
  9. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_bayes_integral_integrable line 73
  10. lemma OAI.ThreeState.TreeClauses.Experiment.integral_discreteMarginal_integrable line 86
  11. lemma OAI.ThreeState.TreeClauses.Experiment.estimator_tv_lower_integrable line 95
  12. lemma OAI.ThreeState.TreeClauses.Experiment.product_sum_integrable line 152
  13. lemma OAI.ThreeState.TreeClauses.Experiment.product_square_sum_integrable line 158
  14. lemma OAI.ThreeState.TreeClauses.Experiment.integral_product_sum_integrable line 165
  15. lemma OAI.ThreeState.TreeClauses.Experiment.integral_product_sq_sum_integrable line 173
  16. lemma OAI.ThreeState.TreeClauses.Experiment.sigmaPMF_integrable line 186
  17. lemma OAI.ThreeState.TreeClauses.Experiment.integral_sigmaPMF_integrable line 196