OAI/Computability/PerfectCompleteness/Foundations/StoppedProjectedOldRecord.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.StoppedProjectedOldRecord.fixed_old_probability line 27
2. abbrev OAI.PerfectCompleteness.StoppedProjectedOldRecord.OldRecord line 84
3. def OAI.PerfectCompleteness.StoppedProjectedOldRecord.arrayRecord line 98
4. def OAI.PerfectCompleteness.StoppedProjectedOldRecord.baseProbability line 104
5. theorem OAI.PerfectCompleteness.StoppedProjectedOldRecord.base_probability_eq_pair line 116
6. abbrev OAI.PerfectCompleteness.StoppedProjectedOldRecord.pairLaw line 149
7. theorem OAI.PerfectCompleteness.StoppedProjectedOldRecord.pair_probability_eq_mean line 157
8. theorem OAI.PerfectCompleteness.StoppedProjectedOldRecord.original_probability_eq_mean line 176
9. theorem OAI.PerfectCompleteness.StoppedProjectedOldRecord.original_oldRecord_law line 229
10. theorem OAI.PerfectCompleteness.StoppedProjectedOldRecord.global_oldRecord_law line 264