OAI/Computability/PerfectCompleteness/Sampling/SourceChildKernelMarginalLemmas.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.SourceChildKernelMarginal.nestedKernel_sources line 18
  2. def OAI.PerfectCompleteness.SourceChildKernelMarginal.sources line 39
  3. theorem OAI.PerfectCompleteness.SourceChildKernelMarginal.childrenLaw_sources line 45
  4. theorem OAI.PerfectCompleteness.SourceChildKernelMarginal.originalLaw_sources line 73
  5. def OAI.PerfectCompleteness.SourceChildNativeLaw.falseFlag line 100
  6. def OAI.PerfectCompleteness.SourceChildNativeLaw.pullback line 109
  7. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.pullback_false line 117
  8. def OAI.PerfectCompleteness.SourceChildNativeLaw.physicalLeft line 131
  9. def OAI.PerfectCompleteness.SourceChildNativeLaw.decodeLeft line 136
  10. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.decodeLeft_eq_leftChildren line 142
  11. def OAI.PerfectCompleteness.SourceChildNativeLaw.leftLaw line 148
  12. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.physicalLaw_left line 156
  13. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.kernel_decodeLeft line 183
  14. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.leftLaw_false line 195
  15. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.kernel_decodeLeft_false line 202
  16. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.kernels_decodeLeft line 208
  17. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.kernels_leftChildren line 217
  18. theorem OAI.PerfectCompleteness.SourceChildNativeLaw.kernels_leftChildren_false line 224