OAI/Geometry/IsometricImmersion/Pulses/PulseFlowDistance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Pulse.scalar_fderiv_coordinate_bound line 14
2. theorem OAI.SmoothLocal.Pulse.quotient_change_from_origin line 30
3. theorem OAI.SmoothLocal.Pulse.flow_segment_coordinate_sum line 67
4. theorem OAI.SmoothLocal.Pulse.flow_segment_quotient_near_center line 94
5. theorem OAI.SmoothLocal.Pulse.actual_shear_seed_distance line 122