OAI/Probability/LatticeSurface/Skorokhod/SkorokhodSupport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ConvexSkorokhod.Body line 13
  2. def OAI.ConvexSkorokhod.project line 21
  3. def OAI.ConvexSkorokhod.walk line 24
  4. def OAI.ConvexSkorokhod.regulator line 28
  5. def OAI.ConvexSkorokhod.variation line 31
  6. lemma OAI.ConvexSkorokhod.project_mem line 43
  7. lemma OAI.ConvexSkorokhod.project_variational line 46
  8. lemma OAI.ConvexSkorokhod.walk_mem line 53
  9. lemma OAI.ConvexSkorokhod.regulator_zero line 58
  10. lemma OAI.ConvexSkorokhod.regulator_increment line 60
  11. lemma OAI.ConvexSkorokhod.regulator_normal line 64
  12. lemma OAI.ConvexSkorokhod.ball_normal_impulse line 71
  13. lemma OAI.ConvexSkorokhod.sum_inner_increment line 90
  14. lemma OAI.ConvexSkorokhod.sum_inner_energy line 99