OAI/Probability/Ballisticity/Estimates/NoDropApproxError.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.noDropFinite_lower_rows line 83
2. def OAI.DirectionalTransience.noDropApproxError line 97
3. lemma OAI.DirectionalTransience.noDropApproxError_translation line 101
4. lemma OAI.DirectionalTransience.noDropApproxError_le_one line 112
5. lemma OAI.DirectionalTransience.noDropApproxError_tendsto line 119
6. lemma OAI.DirectionalTransience.normalizedMeasure_upper_le line 140
7. lemma OAI.DirectionalTransience.levyProkhorov_normalized_map_le line 152
8. lemma OAI.DirectionalTransience.weak_limit_of_uniform_approximation line 179
9. lemma OAI.DirectionalTransience.weightedConditioned_apply line 207
10. lemma OAI.DirectionalTransience.weightedConditioned_mono line 216
11. lemma OAI.DirectionalTransience.weightedConditioned_approx line 224
12. lemma OAI.DirectionalTransience.weightedConditioned_noDrop_mass line 244
13. lemma OAI.DirectionalTransience.weightedConditioned_noDrop_approx line 255