OAI/Geometry/NearbyLagrangian/QuadraticStability.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Positive and negative square stabilization of trivial negative fibrations.

  1. def OAI.NearbyLagrangian.Tubes.scalarCoordinate line 16
  2. lemma OAI.NearbyLagrangian.Tubes.scalarCoordinate_apply line 19
  3. lemma OAI.NearbyLagrangian.Tubes.scalarCoordinate_norm_sq line 21
  4. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_norm_sq line 25
  5. def OAI.NearbyLagrangian.Tubes.negativeSquareCoordinates line 42
  6. def OAI.NearbyLagrangian.Tubes.positiveSquareCoordinates line 45
  7. lemma OAI.NearbyLagrangian.Tubes.negativeSquareCoordinates_norm_sq line 48
  8. lemma OAI.NearbyLagrangian.Tubes.positiveSquareCoordinates_norm_sq line 54
  9. lemma OAI.NearbyLagrangian.Tubes.standardForm_one_zero line 60
  10. lemma OAI.NearbyLagrangian.Tubes.standardForm_zero_one line 67
  11. def OAI.NearbyLagrangian.Tubes.addNegativeOne line 74
  12. def OAI.NearbyLagrangian.Tubes.addPositiveOne line 77
  13. lemma OAI.NearbyLagrangian.Tubes.addNegativeOne_apply line 80
  14. lemma OAI.NearbyLagrangian.Tubes.addPositiveOne_apply line 87
  15. lemma OAI.NearbyLagrangian.Tubes.squareComposition_old line 94
  16. lemma OAI.NearbyLagrangian.Tubes.squareComposition_negative line 110
  17. lemma OAI.NearbyLagrangian.Tubes.squareComposition_positive line 122
  18. lemma OAI.NearbyLagrangian.Tubes.standardForm_one_one line 129
  19. lemma OAI.NearbyLagrangian.Tubes.addPositiveNegative_eq_stabilize line 135
  20. theorem OAI.NearbyLagrangian.Tubes.negativeTrivial_iff_sphere line 159
  21. theorem OAI.NearbyLagrangian.Tubes.NegativeTrivial.addPositiveOne line 178
  22. theorem OAI.NearbyLagrangian.Tubes.NegativeTrivial.addNegativeOne line 198
  23. theorem OAI.NearbyLagrangian.Tubes.NegativeTrivial.stabilize line 220
  24. theorem OAI.NearbyLagrangian.Tubes.NegativeTrivial.stabilizeFor line 227
  25. lemma OAI.NearbyLagrangian.Tubes.negativeTrivial_tubeCast_iff line 245
  26. theorem OAI.NearbyLagrangian.Tubes.StableNegativeTrivial.stabilize line 252
  27. theorem OAI.NearbyLagrangian.Tubes.StableNegativeTrivial.addBalanced line 276
  28. theorem OAI.NearbyLagrangian.Tubes.StableNegativeTrivial.addBalancedFor line 284