OAI/Probability/LatticeSurface/Brownian/VectorRiemannGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ConvexSkorokhod.unitGrid line 10
2. def OAI.ConvexSkorokhod.vectorStep line 13
3. lemma OAI.ConvexSkorokhod.unitGrid_val line 22
4. lemma OAI.ConvexSkorokhod.unitGrid_zero line 25
5. lemma OAI.ConvexSkorokhod.grid_cell_unique line 28
6. lemma OAI.ConvexSkorokhod.exists_grid_cell line 47
7. lemma OAI.ConvexSkorokhod.grid_cell_dist line 67
8. lemma OAI.ConvexSkorokhod.vectorStep_eq_cell line 78
9. lemma OAI.ConvexSkorokhod.vectorStep_zero line 90