OAI/Probability/ThreeStateClauses/RegularLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Regular Law.

  1. def OAI.ThreeState.TreeClauses.Tree.RegularObservation line 18
  2. instance OAI.ThreeState.TreeClauses.Tree.regularObservationFintype line 22
  3. instance OAI.ThreeState.TreeClauses.Tree.regularObservationMeasurable line 27
  4. instance OAI.ThreeState.TreeClauses.Tree.regularObservationSingleton line 31
  5. instance OAI.ThreeState.TreeClauses.Tree.observationCountable line 36
  6. instance OAI.ThreeState.TreeClauses.Tree.observationMeasurable line 41
  7. instance OAI.ThreeState.TreeClauses.Tree.observationSingleton line 42
  8. def OAI.ThreeState.TreeClauses.Tree.regularLaw line 45
  9. def OAI.ThreeState.TreeClauses.Tree.forgetRegular line 50
  10. lemma OAI.ThreeState.TreeClauses.Tree.productPMF_list line 54
  11. lemma OAI.ThreeState.TreeClauses.Tree.regularLaw_forget line 74
  12. def OAI.ThreeState.TreeClauses.Tree.regularExpansion line 89
  13. lemma OAI.ThreeState.TreeClauses.Tree.regularLaw_degrades line 94