OAI/Computability/PerfectCompleteness/Foundations/StoppedProjectedCoarseLemmas.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PerfectCompleteness.StoppedProjectedCoarse.pairLaw line 94
2. theorem OAI.PerfectCompleteness.StoppedProjectedCoarse.original_observe_law line 101
3. theorem OAI.PerfectCompleteness.StoppedProjectedCoarse.totalVariation_le_pair line 129
4. theorem OAI.PerfectCompleteness.StoppedProjectedPairMean.proper_pair_law line 174
5. def OAI.PerfectCompleteness.StoppedProjectedPairMean.fixedPair line 216
6. theorem OAI.PerfectCompleteness.StoppedProjectedPairMean.fixedPair_eq line 236
7. theorem OAI.PerfectCompleteness.StoppedProjectedPairMean.pairedLaw_eq_mixture line 253