OAI/Analysis/IrrationalRotation/Couplings/ConditionalCrossingAvoidance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CrossingAvoidance.kernel_iIndepSet_ae line 16
2. theorem OAI.Invariant233.CrossingAvoidance.kernel_avoid_le_exp line 26
3. theorem OAI.Invariant233.CrossingAvoidance.kernel_bad_le_exp_intensity line 36
4. theorem OAI.Invariant233.CrossingAvoidance.kernel_bad_le_exp_intensity_on line 59
5. theorem OAI.Invariant233.CrossingAvoidance.iCondIndepSet_ae_condExpKernel line 92
6. theorem OAI.Invariant233.CrossingAvoidance.conditional_bad_le_exp_intensity line 101
7. theorem OAI.Invariant233.CrossingAvoidance.conditional_bad_le_exp_of_endpoint line 134