OAI/Computability/PerfectCompleteness/Sampling/SamplerCompositionLaws.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PerfectCompleteness.SamplerComposition.expansionSpaceNonempty line 20
  2. instance OAI.PerfectCompleteness.SamplerComposition.expandedTapeNonempty line 25
  3. theorem OAI.PerfectCompleteness.SamplerComposition.expansionSpace_finite line 32
  4. instance OAI.PerfectCompleteness.SamplerComposition.expansionSpaceFinite line 54
  5. instance OAI.PerfectCompleteness.SamplerComposition.expansionSpaceFintype line 59
  6. instance OAI.PerfectCompleteness.SamplerComposition.expandedTapeFintype line 64
  7. def OAI.PerfectCompleteness.SamplerComposition.expandedTapeLaw line 71
  8. theorem OAI.PerfectCompleteness.SamplerComposition.expandedTapeLaw_eq_uniform line 80
  9. theorem OAI.PerfectCompleteness.SamplerComposition.expand_tapeLaw line 89
  10. def OAI.PerfectCompleteness.SamplerComposition.factorLaw line 97
  11. theorem OAI.PerfectCompleteness.SamplerComposition.collapseExpanded_expandedTapeLaw line 103
  12. theorem OAI.PerfectCompleteness.SamplerComposition.collapseSuffix_tapeLaw line 113
  13. theorem OAI.PerfectCompleteness.SamplerComposition.law_append line 123