OAI/Computability/PerfectCompleteness/Foundations/StoppedProjectedPhysicalAdvice.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.physicalSampleFintype line 16
2. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.Outer line 33
3. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.Advice line 36
4. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.Sample line 43
5. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.RawSample line 48
6. def OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.read line 93
7. def OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.law line 108
8. def OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.rawLaw line 114
9. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.fiber_read_law line 127
10. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.read_law line 189
11. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalAdvice.expectation_read line 219