OAI/Computability/PerfectCompleteness/Sampling/SamplerComposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SamplerComposition.ExpansionSpace line 18
  2. abbrev OAI.PerfectCompleteness.SamplerComposition.ExpandedTape line 27
  3. def OAI.PerfectCompleteness.SamplerComposition.zeroFactor line 31
  4. def OAI.PerfectCompleteness.SamplerComposition.zeroExpandedTape line 41
  5. def OAI.PerfectCompleteness.SamplerComposition.expandedSubTape line 45
  6. def OAI.PerfectCompleteness.SamplerComposition.expand line 52
  7. def OAI.PerfectCompleteness.SamplerComposition.flatten line 63
  8. theorem OAI.PerfectCompleteness.SamplerComposition.flatten_expand line 74
  9. theorem OAI.PerfectCompleteness.SamplerComposition.expand_flatten line 90
  10. def OAI.PerfectCompleteness.SamplerComposition.expandEquiv line 110
  11. def OAI.PerfectCompleteness.SamplerComposition.collapseFactor line 118
  12. def OAI.PerfectCompleteness.SamplerComposition.collapseExpanded line 128
  13. def OAI.PerfectCompleteness.SamplerComposition.collapseSuffix line 133
  14. theorem OAI.PerfectCompleteness.SamplerComposition.evaluate_collapseExpanded line 138
  15. theorem OAI.PerfectCompleteness.SamplerComposition.evaluate_collapseSuffix line 156