OAI/Combinatorics/KMedianRecovery/Recovery/Failure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.FailureBudget.failure line 7
2. lemma OAI.MetricKMedianRecovery.FailureBudget.failure_pos line 10
3. lemma OAI.MetricKMedianRecovery.FailureBudget.failure_le_margin line 14
4. lemma OAI.MetricKMedianRecovery.FailureBudget.failure_le_power line 20
5. lemma OAI.MetricKMedianRecovery.FailureBudget.expectation_margin line 37
6. lemma OAI.MetricKMedianRecovery.FailureBudget.failure_log line 42