OAI/Computability/PerfectCompleteness/Decoding/ChildBlockProjection.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ChildBlockProjection.nodeProjection line 20
  2. theorem OAI.PerfectCompleteness.ChildBlockProjection.restrictNode_projection line 26
  3. def OAI.PerfectCompleteness.ChildBlockProjection.squarePullback line 32
  4. theorem OAI.PerfectCompleteness.ChildBlockProjection.squarePullback_apply line 40
  5. theorem OAI.PerfectCompleteness.ChildBlockProjection.squarePullback_injective line 45
  6. def OAI.PerfectCompleteness.ChildBlockProjection.arraysPullback line 53
  7. theorem OAI.PerfectCompleteness.ChildBlockProjection.arraysPullback_apply line 64
  8. theorem OAI.PerfectCompleteness.ChildBlockProjection.arraysPullback_injective line 71
  9. theorem OAI.PerfectCompleteness.ChildBlockProjection.fullJoint_pullback line 79
  10. def OAI.PerfectCompleteness.ChildBlockProjection.rawPullback line 84
  11. theorem OAI.PerfectCompleteness.ChildBlockProjection.rawPullback_injective line 100
  12. def OAI.PerfectCompleteness.ChildBlockProjection.evaluate line 111
  13. theorem OAI.PerfectCompleteness.ChildBlockProjection.evaluate_pullback line 116
  14. def OAI.PerfectCompleteness.ChildBlockProjection.liftedLaw line 121
  15. instance OAI.PerfectCompleteness.ChildBlockProjection.liftedRangeFintype line 127
  16. theorem OAI.PerfectCompleteness.ChildBlockProjection.liftedLaw_eq_uniform_range line 131
  17. theorem OAI.PerfectCompleteness.ChildBlockProjection.liftedLaw_evaluate line 142
  18. def OAI.PerfectCompleteness.ChildBlockProjection.mixtureLaw line 151
  19. theorem OAI.PerfectCompleteness.ChildBlockProjection.mixtureLaw_weight line 159
  20. def OAI.PerfectCompleteness.ChildBlockProjection.replacementLaws line 171
  21. theorem OAI.PerfectCompleteness.ChildBlockProjection.observed_variation line 179
  22. theorem OAI.PerfectCompleteness.ChildBlockProjection.adaptive_selection line 200