OAI/Geometry/NearbyLagrangian/SphereHeights.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Sphere height derivatives and uniform scale separation estimates.

  1. def OAI.NearbyLagrangian.SphereDirection.height line 20
  2. def OAI.NearbyLagrangian.SphereDirection.direction line 22
  3. lemma OAI.NearbyLagrangian.SphereDirection.inner_direction line 24
  4. def OAI.NearbyLagrangian.SphereDirection.line line 30
  5. lemma OAI.NearbyLagrangian.SphereDirection.line_ne_zero line 33
  6. def OAI.NearbyLagrangian.SphereDirection.curve line 42
  7. lemma OAI.NearbyLagrangian.SphereDirection.curve_zero line 47
  8. theorem OAI.NearbyLagrangian.SphereDirection.contMDiff_curve line 51
  9. theorem OAI.NearbyLagrangian.SphereDirection.hasDerivAt_curve line 68
  10. theorem OAI.NearbyLagrangian.SphereDirection.hasDerivAt_height_curve line 83
  11. def OAI.NearbyLagrangian.SphereDirection.tangent line 92
  12. theorem OAI.NearbyLagrangian.SphereDirection.deriv_curve_eq line 95
  13. def OAI.NearbyLagrangian.ScalarMixed.momentum line 130
  14. theorem OAI.NearbyLagrangian.ScalarMixed.momentum_eq_baseDerivative line 136
  15. theorem OAI.NearbyLagrangian.ScalarMixed.contMDiffAt_momentum line 144
  16. theorem OAI.NearbyLagrangian.ScalarMixed.exists_uniform_mixed_bound line 165
  17. lemma OAI.NearbyLagrangian.HeightSeparation.contMDiff_height line 212
  18. def OAI.NearbyLagrangian.HeightSeparation.scaleDerivative line 216
  19. lemma OAI.NearbyLagrangian.HeightSeparation.scaleDerivative_height line 220
  20. lemma OAI.NearbyLagrangian.HeightSeparation.height_direction_lower line 237
  21. theorem OAI.NearbyLagrangian.HeightSeparation.exists_momentum_scale_bound line 244
  22. lemma OAI.NearbyLagrangian.Tubes.standardForm_fderiv_apply line 299
  23. theorem OAI.NearbyLagrangian.Tubes.standardForm_gradient_injective line 322