OAI/Probability/Ballisticity/Estimates/WeightedConditioned.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.weightedConditioned line 77
2. lemma OAI.DirectionalTransience.weightedConditioned_le line 81
3. lemma OAI.DirectionalTransience.weightedConditioned_apply_subset line 90
4. lemma OAI.DirectionalTransience.weightedConditioned_highWord_factor line 97
5. lemma OAI.DirectionalTransience.weightedConditioned_highSuffix line 148
6. lemma OAI.DirectionalTransience.levyProkhorov_map_distance_le line 186
7. lemma OAI.DirectionalTransience.weak_map_of_varying_close line 204