OAI/Computability/PerfectCompleteness/Reduction/FixedComparisonErrorsLemmas.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.FixedComparisonErrors.comparison_errors line 18
2. theorem OAI.PerfectCompleteness.HierarchicalFixedAdvice.rows_positive line 100
3. theorem OAI.PerfectCompleteness.HierarchicalFixedAdvice.adviceFactor_eq line 103
4. theorem OAI.PerfectCompleteness.HierarchicalFixedAdvice.paired_error_small line 110
5. theorem OAI.PerfectCompleteness.HierarchicalFixedAdvice.coarse_error_small line 115
6. theorem OAI.PerfectCompleteness.HierarchicalFixedAdvice.prediction_difference line 127
7. theorem OAI.PerfectCompleteness.HierarchicalFixedAdvice.good_record_mass_ge line 166
8. theorem OAI.PerfectCompleteness.HierarchicalFixedProjectedMeeting.meeting_probability_lower line 242