OAI/Probability/ThreeStateClauses/OffspringLaws.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Offspring Laws.

  1. def OAI.ThreeState.TreeClauses.Tree.OrderedObservation line 17
  2. instance OAI.ThreeState.TreeClauses.Tree.orderedObservationCountable line 21
  3. instance OAI.ThreeState.TreeClauses.Tree.orderedObservationMeasurable line 26
  4. instance OAI.ThreeState.TreeClauses.Tree.orderedObservationSingleton line 31
  5. def OAI.ThreeState.TreeClauses.Tree.orderedLaw line 36
  6. def OAI.ThreeState.TreeClauses.Tree.forgetOrdered line 42
  7. lemma OAI.ThreeState.TreeClauses.Tree.orderedLaw_forget line 46
  8. def OAI.ThreeState.TreeClauses.Tree.orderedExpansion line 64
  9. lemma OAI.ThreeState.TreeClauses.Tree.orderedLaw_degrades line 69
  10. def OAI.ThreeState.TreeClauses.Tree.offspringPosteriorLaw line 89
  11. lemma OAI.ThreeState.TreeClauses.Tree.offspringPosteriorLaw_probability line 93
  12. lemma OAI.ThreeState.TreeClauses.Tree.sigmaPMF_map_components line 116
  13. def OAI.ThreeState.TreeClauses.Tree.relabelOrdered line 125
  14. lemma OAI.ThreeState.TreeClauses.Tree.orderedLaw_permute line 129
  15. def OAI.ThreeState.TreeClauses.Tree.orderedNoise line 148
  16. lemma OAI.ThreeState.TreeClauses.Tree.orderedLaw_noise line 155
  17. lemma OAI.ThreeState.TreeClauses.Tree.ordered_channel_mu_le line 189
  18. lemma OAI.ThreeState.TreeClauses.Experiment.degrading_offspring_fixed_point line 208