OAI/Probability/Ballisticity/Estimates/FinitePolicyFailure.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.DirectionalTransience.finitePolicyPMF_prefix_eventline 14 - lemma
OAI.DirectionalTransience.finitePolicyPMF_fresh_failureline 27 - lemma
OAI.DirectionalTransience.finitePolicyPMF_failure_unionline 53 - lemma
OAI.DirectionalTransience.curveFailure_rowsline 97 - lemma
OAI.DirectionalTransience.curveFailure_translationline 106 - lemma
OAI.DirectionalTransience.alignedCurvePolicy_failure_unionline 127 - lemma
OAI.DirectionalTransience.curvePolicy_actual_failureline 153