OAI/Probability/LatticeSurface/Skorokhod/SkorokhodSegment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ConvexSkorokhod.variation_nonneg line 12
2. lemma OAI.ConvexSkorokhod.variation_add line 15
3. lemma OAI.ConvexSkorokhod.variation_mono line 21
4. lemma OAI.ConvexSkorokhod.walk_shift line 29
5. lemma OAI.ConvexSkorokhod.regulator_shift line 38
6. lemma OAI.ConvexSkorokhod.variation_sub_const line 45
7. lemma OAI.ConvexSkorokhod.regulator_shift_variation line 52
8. lemma OAI.ConvexSkorokhod.walk_constant line 63
9. lemma OAI.ConvexSkorokhod.walk_segment_displacement line 70