OAI/Probability/ThreeStateClauses/ObservedMixtures.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Observed Mixtures.

  1. def OAI.ThreeState.TreeClauses.Experiment.mixtureProbability line 18
  2. lemma OAI.ThreeState.TreeClauses.Experiment.integral_mixtureProbability line 23
  3. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_hasSum_real line 31
  4. lemma OAI.ThreeState.TreeClauses.Experiment.mixture_balanced line 37
  5. lemma OAI.ThreeState.TreeClauses.Experiment.mixture_symmetric line 43
  6. def OAI.ThreeState.TreeClauses.Experiment.mixtureLaw line 53
  7. def OAI.ThreeState.TreeClauses.Experiment.offspringLaw line 58
  8. lemma OAI.ThreeState.TreeClauses.Experiment.mixture_integrable line 61
  9. lemma OAI.ThreeState.TreeClauses.Experiment.mixtureProbability_tendsto line 71
  10. lemma OAI.ThreeState.TreeClauses.Experiment.offspringLaw_tendsto line 88
  11. def OAI.ThreeState.TreeClauses.Experiment.sigmaPMF line 107
  12. lemma OAI.ThreeState.TreeClauses.Experiment.sigmaPMF_apply line 115
  13. lemma OAI.ThreeState.TreeClauses.Experiment.sigmaPMF_eq_bind line 118
  14. lemma OAI.ThreeState.TreeClauses.Experiment.sigmaPMF_bind line 129
  15. lemma OAI.ThreeState.TreeClauses.Experiment.sigmaPMF_map line 135
  16. lemma OAI.ThreeState.TreeClauses.Experiment.sigmaPMF_bind_components line 140
  17. lemma OAI.ThreeState.TreeClauses.Experiment.discreteSigma_marginal line 147
  18. lemma OAI.ThreeState.TreeClauses.Experiment.discreteSigma_weight line 155
  19. lemma OAI.ThreeState.TreeClauses.Experiment.discreteSigma_message line 161
  20. instance OAI.ThreeState.TreeClauses.Experiment.sigmaMeasurableSingleton line 176
  21. lemma OAI.ThreeState.TreeClauses.Experiment.integral_sigmaPMF line 184
  22. lemma OAI.ThreeState.TreeClauses.Experiment.discreteSigma_probability line 193