OAI/Computability/PerfectCompleteness/Foundations/OriginalPrefixContinuation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.sigmaLaw_pushforward line 18
  2. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.product_mixture line 29
  3. abbrev OAI.PerfectCompleteness.OriginalPrefixContinuation.Blocks line 41
  4. abbrev OAI.PerfectCompleteness.OriginalPrefixContinuation.Tape line 45
  5. def OAI.PerfectCompleteness.OriginalPrefixContinuation.tagLaw line 51
  6. def OAI.PerfectCompleteness.OriginalPrefixContinuation.sourceLaw line 56
  7. def OAI.PerfectCompleteness.OriginalPrefixContinuation.rawMap line 64
  8. def OAI.PerfectCompleteness.OriginalPrefixContinuation.averagedSpecial line 70
  9. def OAI.PerfectCompleteness.OriginalPrefixContinuation.blockMixture line 77
  10. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.special_as_continued line 85
  11. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.rawMap_law line 99
  12. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.rawMap_eq_mixture line 120
  13. def OAI.PerfectCompleteness.OriginalPrefixContinuation.observed line 129
  14. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.assemble_rawMap line 136
  15. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.observed_law line 144
  16. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.raw_observed_variation line 156
  17. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.observed_variation line 179
  18. def OAI.PerfectCompleteness.OriginalPrefixContinuation.assembledLaw line 206
  19. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.assembledLaw_eq_mixture line 213
  20. theorem OAI.PerfectCompleteness.OriginalPrefixContinuation.assembledLaw_variation line 228