OAI/Geometry/NearbyLagrangian/SquareCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Split sphere coordinates and equivalences for added quadratic variables.

  1. def OAI.NearbyLagrangian.RadialTopology.splitDomainHomeomorph line 20
  2. def OAI.NearbyLagrangian.RadialTopology.fullSphere line 42
  3. lemma OAI.NearbyLagrangian.RadialTopology.mem_sphere_of_norm_one line 47
  4. lemma OAI.NearbyLagrangian.RadialTopology.norm_one_of_mem_sphere line 51
  5. def OAI.NearbyLagrangian.RadialTopology.fullSphereHomeomorph line 54
  6. lemma OAI.NearbyLagrangian.RadialTopology.norm_one_of_split line 65
  7. lemma OAI.NearbyLagrangian.RadialTopology.full_suspension_condition line 74
  8. def OAI.NearbyLagrangian.RadialTopology.suspensionFullSphereHomeomorph line 86
  9. def OAI.NearbyLagrangian.RadialTopology.negativeSquareCoordinateHomeomorph line 98
  10. def OAI.NearbyLagrangian.RadialTopology.positiveSquareCoordinateHomeomorph line 107
  11. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.squareExtend line 122
  12. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.squareExtend_negative_apply line 128
  13. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.squareExtend_positive_apply line 134
  14. def OAI.NearbyLagrangian.RadialTopology.positiveSquareCoordinatesEquiv line 149
  15. def OAI.NearbyLagrangian.RadialTopology.suspendTrivialization line 157
  16. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_uniform_sphere_gradient_lower line 181
  17. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.negativeSquare_equiv line 191