OAI/Geometry/NearbyLagrangian/HomogeneousCritical.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gradient bounds and regular radial parametrization of critical loci.

  1. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.gradient_bounds line 16
  2. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.unit_ne_zero line 51
  3. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.angularPosition line 55
  4. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_smul_angularPosition line 62
  5. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.angularPosition_radialSolution line 67
  6. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_direction line 76
  7. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_radialSolution line 82
  8. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.CriticalLocus line 88
  9. instance OAI.NearbyLagrangian.Tubes.RegularHomogeneous.(instance at line 91) line 91
  10. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.critical_ne_zero line 95
  11. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.critical_gradient_norm line 102
  12. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.critical_radial_recovery line 107
  13. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.criticalHomeomorph line 124
  14. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_family_gradient line 146
  15. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.uniform_gradient_bounds line 155
  16. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_tangent_derivative line 196
  17. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.angular_zero_regular line 211