OAI/Probability/Ballisticity/Coupling/FreshBudgetEvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.fresh_random_budget_mass_lt line 13
2. lemma OAI.DirectionalTransience.fresh_layer_diagonal_bound line 53
3. lemma OAI.DirectionalTransience.fresh_layer_profile_event_bound line 78
4. lemma OAI.DirectionalTransience.seedSeparatedMass_joint_upper line 103
5. lemma OAI.DirectionalTransience.fresh_random_seed_failure line 114
6. lemma OAI.DirectionalTransience.seedSeparatedRaw_measurable line 126
7. theorem OAI.DirectionalTransience.adapted_separated_seeds line 131