OAI/Computability/PerfectCompleteness/Foundations/HierarchicalProjectedExperimentLemmas.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HierarchicalProjectedExperiment.Sample line 30
  2. def OAI.PerfectCompleteness.HierarchicalProjectedExperiment.originalLaw line 33
  3. def OAI.PerfectCompleteness.HierarchicalProjectedExperiment.arrays line 38
  4. def OAI.PerfectCompleteness.HierarchicalProjectedExperiment.experiment line 44
  5. abbrev OAI.PerfectCompleteness.HierarchicalProjectedExperiment.Advice line 58
  6. abbrev OAI.PerfectCompleteness.HierarchicalProjectedExperiment.RawSample line 60
  7. def OAI.PerfectCompleteness.HierarchicalProjectedExperiment.rawLaw line 64
  8. def OAI.PerfectCompleteness.HierarchicalProjectedExperiment.rawRead line 71
  9. theorem OAI.PerfectCompleteness.HierarchicalProjectedExperiment.rawRead_expectation line 78
  10. theorem OAI.PerfectCompleteness.HierarchicalProjectedExperiment.rawRead_law line 99
  11. theorem OAI.PerfectCompleteness.HierarchicalProjectedExperiment.experiment_rawRead_law line 112
  12. abbrev OAI.PerfectCompleteness.HierarchicalWholeExperiment.Sample line 142
  13. def OAI.PerfectCompleteness.HierarchicalWholeExperiment.originalLaw line 145
  14. def OAI.PerfectCompleteness.HierarchicalWholeExperiment.arrays line 150
  15. def OAI.PerfectCompleteness.HierarchicalWholeExperiment.experiment line 155
  16. abbrev OAI.PerfectCompleteness.HierarchicalWholeExperiment.Advice line 169
  17. abbrev OAI.PerfectCompleteness.HierarchicalWholeExperiment.RawSample line 171
  18. def OAI.PerfectCompleteness.HierarchicalWholeExperiment.rawLaw line 175
  19. def OAI.PerfectCompleteness.HierarchicalWholeExperiment.rawRead line 182
  20. theorem OAI.PerfectCompleteness.HierarchicalWholeExperiment.rawRead_expectation line 189
  21. theorem OAI.PerfectCompleteness.HierarchicalWholeExperiment.rawRead_law line 210
  22. theorem OAI.PerfectCompleteness.HierarchicalWholeExperiment.experiment_rawRead_law line 223