OAI/Geometry/NearbyLagrangian/Stabilization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Balanced stabilization, negative fibrations and stable tube classes.

  1. abbrev OAI.NearbyLagrangian.Tubes.Euclidean line 14
  2. def OAI.NearbyLagrangian.Tubes.sumCoordinates line 16
  3. theorem OAI.NearbyLagrangian.Tubes.norm_sq_split line 26
  4. theorem OAI.NearbyLagrangian.Tubes.standardForm_apply line 32
  5. theorem OAI.NearbyLagrangian.Tubes.standardForm_sum line 36
  6. def OAI.NearbyLagrangian.Tubes.tubeSum line 56
  7. def OAI.NearbyLagrangian.Tubes.stabilize line 72
  8. theorem OAI.NearbyLagrangian.Tubes.stabilize_standard line 76
  9. def OAI.NearbyLagrangian.Tubes.stabilizeFor line 85
  10. theorem OAI.NearbyLagrangian.Tubes.stabilizeFor_standard line 89
  11. structure OAI.NearbyLagrangian.Tubes.FiberwiseHomotopyEquiv line 100
  12. def OAI.NearbyLagrangian.Tubes.NegativeTotal line 110
  13. instance OAI.NearbyLagrangian.Tubes.(instance at line 113) line 113
  14. def OAI.NearbyLagrangian.Tubes.negativeProjection line 117
  15. def OAI.NearbyLagrangian.Tubes.NegativeTrivial line 120
  16. def OAI.NearbyLagrangian.Tubes.StableNegativeTrivial line 124
  17. def OAI.NearbyLagrangian.Tubes.StablyNonNull line 127
  18. def OAI.NearbyLagrangian.Tubes.KernelFamilyGoal line 130