OAI/Probability/LatticeSurface/Skorokhod/SkorokhodNormalSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ConvexSkorokhod.normalPartition line 12
2. lemma OAI.ConvexSkorokhod.normal_block_bound line 25
3. lemma OAI.ConvexSkorokhod.normal_coarse_bound line 53
4. lemma OAI.ConvexSkorokhod.mesh_at_sample line 74
5. lemma OAI.ConvexSkorokhod.partition_sample_near line 79