OAI/Probability/LatticeSurface/Dynamics/ProjectionLimitSupport.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ProjectionComparison.pathIncrementline 16 - def
OAI.ProjectionComparison.pathMeshline 19 - def
OAI.ProjectionComparison.pathTailline 23 - lemma
OAI.ProjectionComparison.coordinates_extendFreeline 37 - lemma
OAI.ProjectionComparison.pathMesh_eq_hilbertline 44 - lemma
OAI.ProjectionComparison.extendFree_lipschitzline 66 - lemma
OAI.ProjectionComparison.exists_projection_pathline 78