OAI/Geometry/NearbyLagrangian/BalancedStability.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Balanced stabilization identities and persistence of nonzero stable classes.

  1. lemma OAI.NearbyLagrangian.Tubes.split_fst_apply line 14
  2. lemma OAI.NearbyLagrangian.Tubes.split_snd_apply line 16
  3. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_fst_neg line 19
  4. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_fst_pos line 29
  5. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_snd_neg line 39
  6. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_snd_pos line 49
  7. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_old_succ line 59
  8. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_quadratic_succ line 74
  9. lemma OAI.NearbyLagrangian.Tubes.sumCoordinates_old_zero line 119
  10. theorem OAI.NearbyLagrangian.Tubes.addBalanced_eq_stabilizeFor line 132
  11. def OAI.NearbyLagrangian.Tubes.tubeCast line 163
  12. lemma OAI.NearbyLagrangian.Tubes.tubeCast_rfl line 167
  13. lemma OAI.NearbyLagrangian.Tubes.tubeCast_stabilize line 169
  14. lemma OAI.NearbyLagrangian.Tubes.stabilizeFor_comp line 174
  15. theorem OAI.NearbyLagrangian.Tubes.StablyNonNull.stabilize line 189
  16. theorem OAI.NearbyLagrangian.Tubes.kernel_finite_negative_trivial line 204
  17. theorem OAI.NearbyLagrangian.Tubes.StablyNonNull.addBalanced line 217
  18. theorem OAI.NearbyLagrangian.Tubes.StablyNonNull.addBalancedFor line 222