OAI/Geometry/Symplectic/MorseBounds/SphereForm.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MorseArnold.SphereSymplectic.areaBilinear line 17
  2. lemma OAI.MorseArnold.SphereSymplectic.areaBilinear_apply line 25
  3. def OAI.MorseArnold.SphereSymplectic.areaTrilinear line 28
  4. lemma OAI.MorseArnold.SphereSymplectic.areaTrilinear_apply line 34
  5. def OAI.MorseArnold.SphereSymplectic.tangentInclusion line 37
  6. def OAI.MorseArnold.SphereSymplectic.sphereArea line 40
  7. lemma OAI.MorseArnold.SphereSymplectic.sphereArea_apply line 44
  8. lemma OAI.MorseArnold.SphereSymplectic.sphereArea_alternating line 48
  9. def OAI.MorseArnold.SphereSymplectic.cross line 51
  10. lemma OAI.MorseArnold.SphereSymplectic.inner_formula line 55
  11. lemma OAI.MorseArnold.SphereSymplectic.cross_orthogonal line 60
  12. lemma OAI.MorseArnold.SphereSymplectic.area_cross line 63
  13. lemma OAI.MorseArnold.SphereSymplectic.tangent_orthogonal line 69
  14. lemma OAI.MorseArnold.SphereSymplectic.sphereArea_kernel line 75
  15. lemma OAI.MorseArnold.SphereSymplectic.sphereArea_nondegenerate line 99
  16. def OAI.MorseArnold.SphereSymplectic.chartEmbedding line 105
  17. lemma OAI.MorseArnold.SphereSymplectic.chartEmbedding_smoothAt line 108
  18. lemma OAI.MorseArnold.SphereSymplectic.chartEmbedding_derivative line 115
  19. lemma OAI.MorseArnold.SphereSymplectic.chartSphereArea_apply line 128
  20. lemma OAI.MorseArnold.SphereSymplectic.chartSphereArea_alternating line 135
  21. lemma OAI.MorseArnold.SphereSymplectic.sphereArea_smoothAt line 139
  22. lemma OAI.MorseArnold.SphereSymplectic.derivative_alternating line 168
  23. def OAI.MorseArnold.SphereSymplectic.e2 line 182
  24. lemma OAI.MorseArnold.SphereSymplectic.expand_model2 line 184
  25. lemma OAI.MorseArnold.SphereSymplectic.alternating_skew line 188
  26. lemma OAI.MorseArnold.SphereSymplectic.model2_cyclic_zero line 195
  27. lemma OAI.MorseArnold.SphereSymplectic.sphereArea_closed line 203
  28. theorem OAI.MorseArnold.SphereSymplectic.scaled_standardSphere_symplectic line 212