OAI/Probability/Ballisticity/Coupling/QuenchedConditionalProbability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.quenchedConditionalProbability line 191
2. lemma OAI.DirectionalTransience.measurable_quenchedConditionalProbability line 195
3. lemma OAI.DirectionalTransience.quenchedConditionalProbability_le_one line 200
4. lemma OAI.DirectionalTransience.quenchedConditionalProbability_real_integrable line 204
5. lemma OAI.DirectionalTransience.quenchedConditionalProbability_mean line 213
6. lemma OAI.DirectionalTransience.quenched_good_mass_identity line 222
7. theorem OAI.DirectionalTransience.quenched_good_mass_bad_probability line 239
8. lemma OAI.DirectionalTransience.positive_lower_quantile line 275