OAI/Probability/Ballisticity/Crossings/BadCrossingLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.klDiv_le_log_of_domination line 13
2. lemma OAI.DirectionalTransience.cond_klDiv_le line 47
3. def OAI.DirectionalTransience.badCrossingEvent line 59
4. lemma OAI.DirectionalTransience.badCrossingEvent_measurable line 62
5. lemma OAI.DirectionalTransience.badCrossingEvent_pos line 66
6. lemma OAI.DirectionalTransience.badCrossing_cond_entropy line 74
7. lemma OAI.DirectionalTransience.badCrossing_cond_drop line 85