OAI/Geometry/Symplectic/MorseBounds/LocalCorrection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MorseArnold.LocalCorrection.delta line 19
  2. def OAI.MorseArnold.LocalCorrection.K line 22
  3. def OAI.MorseArnold.LocalCorrection.LocalModel line 26
  4. def OAI.MorseArnold.LocalCorrection.CorrectionObligation line 47
  5. lemma OAI.MorseArnold.LocalCorrection.rotate_add line 78
  6. lemma OAI.MorseArnold.LocalCorrection.quad_add line 81
  7. lemma OAI.MorseArnold.LocalCorrection.exterior_add line 85
  8. lemma OAI.MorseArnold.LocalCorrection.exterior_inverse line 89
  9. lemma OAI.MorseArnold.LocalCorrection.quadratic_invariant line 93
  10. lemma OAI.MorseArnold.LocalCorrection.quadratic_msmooth line 98
  11. lemma OAI.MorseArnold.LocalCorrection.quadratic_hamiltonian line 105
  12. theorem OAI.MorseArnold.LocalCorrection.zero_prod_toSpanSingleton line 127
  13. lemma OAI.MorseArnold.LocalCorrection.quadratic_integral line 137
  14. lemma OAI.MorseArnold.LocalCorrection.rescale_integral line 149
  15. lemma OAI.MorseArnold.LocalCorrection.rescale_smooth line 165
  16. lemma OAI.MorseArnold.LocalCorrection.hamiltonian_scale line 172
  17. theorem OAI.MorseArnold.LocalCorrection.correctionObligation line 183