OAI/Computability/PerfectCompleteness/Construction/StoppedProjectedBuckets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.Base line 29
  2. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.key line 31
  3. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.lowerPath line 34
  4. def OAI.PerfectCompleteness.StoppedProjectedBuckets.chosen line 37
  5. def OAI.PerfectCompleteness.StoppedProjectedBuckets.continuation line 40
  6. theorem OAI.PerfectCompleteness.StoppedProjectedBuckets.lowerPath_eq_step line 44
  7. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.projected line 49
  8. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.projection line 53
  9. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.Exterior line 57
  10. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.Descriptor line 62
  11. def OAI.PerfectCompleteness.StoppedProjectedBuckets.exteriorLaw line 65
  12. def OAI.PerfectCompleteness.StoppedProjectedBuckets.externalLaw line 71
  13. def OAI.PerfectCompleteness.StoppedProjectedBuckets.background line 86
  14. def OAI.PerfectCompleteness.StoppedProjectedBuckets.scalarLaw line 96
  15. abbrev OAI.PerfectCompleteness.StoppedProjectedBuckets.experiment line 110
  16. theorem OAI.PerfectCompleteness.StoppedProjectedBuckets.rows_positive line 115
  17. def OAI.PerfectCompleteness.StoppedProjectedBuckets.usefulProbability line 119
  18. theorem OAI.PerfectCompleteness.StoppedProjectedBuckets.usefulProbability_eq_mean line 127