OAI/Computability/PerfectCompleteness/Construction/OriginalHiddenChild.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalHiddenChild.sigmaLaw_pushforward line 18
  2. theorem OAI.PerfectCompleteness.OriginalHiddenChild.product_mixture line 29
  3. abbrev OAI.PerfectCompleteness.OriginalHiddenChild.Blocks line 41
  4. abbrev OAI.PerfectCompleteness.OriginalHiddenChild.Tape line 45
  5. def OAI.PerfectCompleteness.OriginalHiddenChild.sourceLaw line 50
  6. def OAI.PerfectCompleteness.OriginalHiddenChild.rawMap line 58
  7. def OAI.PerfectCompleteness.OriginalHiddenChild.continuationLaw line 64
  8. def OAI.PerfectCompleteness.OriginalHiddenChild.averagedSpecial line 68
  9. def OAI.PerfectCompleteness.OriginalHiddenChild.blockMixture line 75
  10. theorem OAI.PerfectCompleteness.OriginalHiddenChild.special_as_continued line 81
  11. theorem OAI.PerfectCompleteness.OriginalHiddenChild.rawMap_law line 95
  12. theorem OAI.PerfectCompleteness.OriginalHiddenChild.rawMap_eq_mixture line 122
  13. def OAI.PerfectCompleteness.OriginalHiddenChild.observed line 130
  14. theorem OAI.PerfectCompleteness.OriginalHiddenChild.assemble_rawMap line 136
  15. theorem OAI.PerfectCompleteness.OriginalHiddenChild.observed_law line 144
  16. theorem OAI.PerfectCompleteness.OriginalHiddenChild.raw_observed_variation line 155
  17. theorem OAI.PerfectCompleteness.OriginalHiddenChild.observed_variation line 176