OAI/Probability/Ballisticity/Coupling/WeakLimitBoundedFreshMap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.weak_limit_of_bounded_fresh_map line 80
2. lemma OAI.DirectionalTransience.weightedConditioned_finite line 110
3. lemma OAI.DirectionalTransience.normalized_weightedConditioned_highSuffix line 116
4. lemma OAI.DirectionalTransience.normalized_weightedConditioned_le line 130