OAI/Probability/LatticeSurface/Skorokhod/SkorokhodUniquenessSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ConvexSkorokhod.NormalPartitionCondition line 12
2. lemma OAI.ConvexSkorokhod.uniform_grid_mem line 28
3. lemma OAI.ConvexSkorokhod.grid_variation_le line 35
4. lemma OAI.ConvexSkorokhod.normal_cutoff line 47
5. lemma OAI.ConvexSkorokhod.discrete_left_energy line 59
6. lemma OAI.ConvexSkorokhod.discrete_normal_contraction line 71