OAI/Probability/Ballisticity/Estimates/SingleThreat.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.noDropMass_le_budget_bad line 12
2. def OAI.DirectionalTransience.budgetThreatEvent line 38
3. lemma OAI.DirectionalTransience.budgetThreatEvent_subset_ae line 42
4. lemma OAI.DirectionalTransience.single_budget_threat_bound line 57
5. lemma OAI.DirectionalTransience.annealed_noDrop_event_le_conditioned line 80
6. lemma OAI.DirectionalTransience.annealed_median_failure_bound line 93