OAI/Probability/Ballisticity/Estimates/PolicyGoodMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.measurable_pmf_dependent_event line 14
2. lemma OAI.DirectionalTransience.finitePolicy_length_mass line 25
3. lemma OAI.DirectionalTransience.probability_three_cover line 37
4. lemma OAI.DirectionalTransience.ennreal_half_good line 47
5. lemma OAI.DirectionalTransience.policy_good_mass line 55
6. lemma OAI.DirectionalTransience.low_mass_probability line 71
7. lemma OAI.DirectionalTransience.policySafe_measurable line 96
8. lemma OAI.DirectionalTransience.curvePolicy_atom_measurable line 103
9. lemma OAI.DirectionalTransience.curvePolicy_failure_measurable line 114
10. lemma OAI.DirectionalTransience.curvePolicy_fixed_event_measurable line 130