OAI/Probability/Ballisticity/Coupling/StoppedFreshField.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.stoppedRowsEvent_mono line 13
2. lemma OAI.DirectionalTransience.stoppedRowsEvent_measurable line 33
3. theorem OAI.DirectionalTransience.stopped_fresh_joint_map line 39
4. def OAI.DirectionalTransience.upperField line 91
5. lemma OAI.DirectionalTransience.upperField_index_injective line 94
6. lemma OAI.DirectionalTransience.upperField_measurable_rows line 103
7. lemma OAI.DirectionalTransience.upperField_map line 114