OAI/Probability/Ballisticity/Estimates/NormalLinearPast.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.pairLinearIncrement line 14
2. lemma OAI.DirectionalTransience.normalJointPast_linear_mean_integrable line 17
3. lemma OAI.DirectionalTransience.normalJointPast_linear_mean line 34
4. lemma OAI.DirectionalTransience.normalJointPast_linear_second_integrable line 53
5. lemma OAI.DirectionalTransience.normalJointPast_linear_second line 73
6. lemma OAI.DirectionalTransience.normalJointPast_linear_absolute_third_bound line 102
7. lemma OAI.DirectionalTransience.pairPastTest_integrable line 141
8. lemma OAI.DirectionalTransience.pairPastPhase_integrable line 148
9. lemma OAI.DirectionalTransience.normalJointPast_integral_quadratic line 156
10. lemma OAI.DirectionalTransience.normalJointPast_taylor_error line 182