OAI/Geometry/NearbyLagrangian/HomogeneousFunctions.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Regular homogeneous functions, gradients, radial solutions and tube spaces.

  1. structure OAI.NearbyLagrangian.Tubes.RegularHomogeneous line 15
  2. instance OAI.NearbyLagrangian.Tubes.RegularHomogeneous.(instance at line 23) line 23
  3. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.SmoothOffZero line 27
  4. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.ext line 30
  5. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.map_zero line 35
  6. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.differentiable line 40
  7. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.euler line 43
  8. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.fderiv_smul line 55
  9. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.jet line 74
  10. instance OAI.NearbyLagrangian.Tubes.RegularHomogeneous.(instance at line 80) line 80
  11. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.jet_injective line 82
  12. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.gradient_smul line 112
  13. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.gradient_zero line 116
  14. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.gradient_ne_zero line 122
  15. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_gradient line 128
  16. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.direction line 131
  17. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialSolution line 143
  18. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialSolution_norm line 146
  19. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialSolution_critical line 154
  20. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialSolution_ne_zero line 164
  21. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.pullback line 178
  22. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.directSum line 191
  23. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.neg line 220
  24. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.positiveSquare line 237
  25. def OAI.NearbyLagrangian.Tubes.standardForm line 254
  26. def OAI.NearbyLagrangian.Tubes.Tube line 262
  27. instance OAI.NearbyLagrangian.Tubes.(instance at line 266) line 266
  28. def OAI.NearbyLagrangian.Tubes.standardTube line 270