OAI/Analysis/RieszRectifiability/Kernel/NormalizedNormalCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.tangentPlaneProjection line 12
2. def OAI.RieszRectifiability.normalizedNormalHeight line 16
3. theorem OAI.RieszRectifiability.tangentPlaneProjection_continuous line 20
4. theorem OAI.RieszRectifiability.normalizedNormalHeight_continuous line 25
5. theorem OAI.RieszRectifiability.normalizedNormalHeight_reconstruct line 30
6. theorem OAI.RieszRectifiability.normal_coordinates_decomposition line 35
7. theorem OAI.RieszRectifiability.physical_projection_distance_eq line 43