OAI/Computability/PerfectCompleteness/Foundations/OriginalExtraCutComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.OriginalExtraCutComparison.product_mixture_pushforward line 18
2. abbrev OAI.PerfectCompleteness.OriginalExtraCutComparison.Record line 35
3. def OAI.PerfectCompleteness.OriginalExtraCutComparison.actualLaw line 39
4. def OAI.PerfectCompleteness.OriginalExtraCutComparison.referenceLaw line 51
5. theorem OAI.PerfectCompleteness.OriginalExtraCutComparison.actualLaw_eq_mixture line 58
6. theorem OAI.PerfectCompleteness.OriginalExtraCutComparison.totalVariation_le line 73
7. theorem OAI.PerfectCompleteness.OriginalExtraCutComparison.observed_totalVariation_le line 88