OAI/Computability/PerfectCompleteness/Reduction/FixedStoppedInverseBound.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.clauses line 25
2. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.Outer line 27
3. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.designated line 32
4. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.experiment line 34
5. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.outerLaw line 44
6. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.externalLaw line 48
7. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.background line 56
8. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.scalarLaw line 62
9. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.PairFiber line 88
10. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.PairSample line 93
11. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.backgrounds line 164
12. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.usefulMass line 168
13. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.actualPairs line 176
14. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.referencePairs line 183
15. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.pairedVariation line 189
16. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.coarseVariation line 193
17. abbrev OAI.PerfectCompleteness.FixedStoppedInverseBound.expectedMeeting line 204
18. theorem OAI.PerfectCompleteness.FixedStoppedInverseBound.expectedMeeting_ge_gamma line 211