OAI/Probability/ThreeStateClauses/DiscreteLaw.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Discrete Law.

  1. def OAI.ThreeState.TreeClauses.Experiment.uniformSpin line 18
  2. lemma OAI.ThreeState.TreeClauses.Experiment.uniformSpin_apply line 22
  3. def OAI.ThreeState.TreeClauses.Experiment.discreteMarginal line 24
  4. def OAI.ThreeState.TreeClauses.Experiment.discreteWeight line 26
  5. lemma OAI.ThreeState.TreeClauses.Experiment.discreteWeight_nonneg line 28
  6. lemma OAI.ThreeState.TreeClauses.Experiment.discreteMarginal_apply line 31
  7. lemma OAI.ThreeState.TreeClauses.Experiment.discreteMarginal_real line 36
  8. lemma OAI.ThreeState.TreeClauses.Experiment.discreteWeight_zero line 44
  9. def OAI.ThreeState.TreeClauses.Experiment.discreteMessage line 50
  10. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_bayes line 62
  11. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_coord line 69
  12. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_real_sum line 73
  13. lemma OAI.ThreeState.TreeClauses.Experiment.discreteCoordinate_integrable line 80
  14. def OAI.ThreeState.TreeClauses.Experiment.discreteProbability line 87
  15. lemma OAI.ThreeState.TreeClauses.Experiment.integral_discreteProbability line 91
  16. lemma OAI.ThreeState.TreeClauses.Experiment.discreteProbability_balanced line 97
  17. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_bounded_integrable line 118
  18. lemma OAI.ThreeState.TreeClauses.Experiment.pmf_measure_bind line 125
  19. lemma OAI.ThreeState.TreeClauses.Experiment.integral_pmf_bind line 132
  20. lemma OAI.ThreeState.TreeClauses.Experiment.integral_pmf_map line 149
  21. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_bayes_integral line 155