OAI/Analysis/IrrationalRotation/Couplings/ConditionalAvoidance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ConditionalAvoidance.measurableSet_filter_selection_eq line 21
2. theorem OAI.Invariant233.ConditionalAvoidance.condProb_compl line 53
3. theorem OAI.Invariant233.ConditionalAvoidance.condProb_nonneg line 68
4. theorem OAI.Invariant233.ConditionalAvoidance.condProb_le_on_of_ae_inter_subset line 74
5. theorem OAI.Invariant233.ConditionalAvoidance.condProb_le_on_of_inter_subset line 95
6. theorem OAI.Invariant233.ConditionalAvoidance.prod_one_sub_le_exp line 101
7. theorem OAI.Invariant233.ConditionalAvoidance.condProb_avoid_eq_prod line 118
8. theorem OAI.Invariant233.ConditionalAvoidance.condProb_avoid_random_selection_le_exp_ae line 140
9. theorem OAI.Invariant233.ConditionalAvoidance.condProb_avoid_random_selection_le_exp line 195
10. theorem OAI.Invariant233.ConditionalAvoidance.condProb_half_selection_le_exp line 209
11. theorem OAI.Invariant233.ConditionalAvoidance.condProb_avoid_intensity_le_exp_ae line 227
12. theorem OAI.Invariant233.ConditionalAvoidance.iCondIndepSet_preimages line 247