OAI/Computability/PerfectCompleteness/Decoding/OriginalCutCollision.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.OriginalCutCollision.PairRecord line 22
2. def OAI.PerfectCompleteness.OriginalCutCollision.oldRecord line 37
3. def OAI.PerfectCompleteness.OriginalCutCollision.oldArrays line 43
4. theorem OAI.PerfectCompleteness.OriginalCutCollision.oldArrays_eq line 48
5. def OAI.PerfectCompleteness.OriginalCutCollision.replacementArrays line 63
6. theorem OAI.PerfectCompleteness.OriginalCutCollision.replacement_background_eq line 71
7. def OAI.PerfectCompleteness.OriginalCutCollision.pairRecord line 84
8. theorem OAI.PerfectCompleteness.OriginalCutCollision.pair_totalVariation_le line 95