OAI/Probability/Ballisticity/Estimates/SharedConditionedPairLawFst.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_fst line 103
2. lemma OAI.DirectionalTransience.sharedPairLaw_swap line 127
3. lemma OAI.DirectionalTransience.sharedNoDropMass_swap line 138
4. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_swap line 145
5. lemma OAI.DirectionalTransience.sharedPairLaw_translation line 155
6. lemma OAI.DirectionalTransience.sharedNoDropMass_translation line 179
7. lemma OAI.DirectionalTransience.sharedConditionedPairLaw_translation line 190
8. lemma OAI.DirectionalTransience.tendstoInDistribution_pullback line 212
9. lemma OAI.DirectionalTransience.sharedNoDropMass_pos line 229
10. lemma OAI.DirectionalTransience.distribution_sequence_tight line 236
11. theorem OAI.DirectionalTransience.shared_first_zero_path_limit line 248