OAI/Probability/Ballisticity/Estimates/CurvePolicyAverageMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.curvePolicy_average_moment line 17
2. lemma OAI.DirectionalTransience.curvePolicy_average_zero_moment line 93
3. lemma OAI.DirectionalTransience.signedCoordinate_zsmul line 124
4. lemma OAI.DirectionalTransience.signedHeight_zsmul_other line 128
5. def OAI.DirectionalTransience.medianDummy line 131
6. lemma OAI.DirectionalTransience.medianDummy_height line 133
7. lemma OAI.DirectionalTransience.medianDummy_coordinate line 136
8. lemma OAI.DirectionalTransience.limsup_nonneg_const_mul line 150