OAI/Computability/PerfectCompleteness/Sampling/OriginalCutPairLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.OriginalCutPairLaw.matrix_reconstruct line 31
2. def OAI.PerfectCompleteness.OriginalCutPairLaw.transportPair line 47
3. theorem OAI.PerfectCompleteness.OriginalCutPairLaw.transportPair_law line 54
4. theorem OAI.PerfectCompleteness.OriginalCutPairLaw.pairRecord_eq line 69
5. def OAI.PerfectCompleteness.OriginalCutPairLaw.directionsLaw line 100
6. theorem OAI.PerfectCompleteness.OriginalCutPairLaw.reference_pair_law line 106
7. theorem OAI.PerfectCompleteness.OriginalCutPairLaw.actual_pair_totalVariation_le line 147