OAI/Geometry/Symplectic/MorseBounds/ProductLocal.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MorseArnold.ProductLocal.LE line 17
  2. abbrev OAI.MorseArnold.ProductLocal.LI line 18
  3. def OAI.MorseArnold.ProductLocal.totalSq line 19
  4. def OAI.MorseArnold.ProductLocal.quadratic line 21
  5. instance OAI.MorseArnold.ProductLocal.productCharts line 24
  6. instance OAI.MorseArnold.ProductLocal.productManifold line 26
  7. def OAI.MorseArnold.ProductLocal.exteriorFlow line 29
  8. def OAI.MorseArnold.ProductLocal.ProductLocalObligation line 30
  9. lemma OAI.MorseArnold.ProductLocal.totalSq_smooth line 65
  10. lemma OAI.MorseArnold.ProductLocal.quadratic_smooth line 66
  11. lemma OAI.MorseArnold.ProductLocal.totalSq_nonneg line 67
  12. lemma OAI.MorseArnold.ProductLocal.norm_le_of_totalSq line 69
  13. lemma OAI.MorseArnold.ProductLocal.in_box_of_totalSq line 81
  14. lemma OAI.MorseArnold.ProductLocal.core_compact line 90
  15. lemma OAI.MorseArnold.ProductLocal.rotatePlane_radius line 97
  16. lemma OAI.MorseArnold.ProductLocal.quadFlow_radius line 102
  17. lemma OAI.MorseArnold.ProductLocal.quadFlow_box line 104
  18. lemma OAI.MorseArnold.ProductLocal.quadFlow_zero line 106
  19. lemma OAI.MorseArnold.ProductLocal.quadFlow_smooth line 108
  20. lemma OAI.MorseArnold.ProductLocal.rotatePlane_fixed line 111
  21. lemma OAI.MorseArnold.ProductLocal.quadFlow_fixed line 125
  22. def OAI.MorseArnold.ProductLocal.fourArea line 138
  23. lemma OAI.MorseArnold.ProductLocal.fourArea_apply line 139
  24. lemma OAI.MorseArnold.ProductLocal.fourArea_nondegenerate line 142
  25. lemma OAI.MorseArnold.ProductLocal.fourArea_chart line 150
  26. def OAI.MorseArnold.ProductLocal.four_symplectic line 162
  27. def OAI.MorseArnold.ProductLocal.promoteX line 185
  28. lemma OAI.MorseArnold.ProductLocal.local_symplectic line 190
  29. def OAI.MorseArnold.ProductLocal.planeVelocity line 225
  30. def OAI.MorseArnold.ProductLocal.quadVelocity line 226
  31. def OAI.MorseArnold.ProductLocal.planePotential line 229
  32. def OAI.MorseArnold.ProductLocal.proj11 line 231
  33. def OAI.MorseArnold.ProductLocal.proj12 line 233
  34. def OAI.MorseArnold.ProductLocal.proj21 line 235
  35. def OAI.MorseArnold.ProductLocal.proj22 line 237
  36. lemma OAI.MorseArnold.ProductLocal.planePotential_deriv line 239
  37. lemma OAI.MorseArnold.ProductLocal.quadratic_deriv line 248
  38. lemma OAI.MorseArnold.ProductLocal.rotatePlane_deriv line 265
  39. lemma OAI.MorseArnold.ProductLocal.quadFlow_ode line 272
  40. lemma OAI.MorseArnold.ProductLocal.totalSq_smul line 281
  41. lemma OAI.MorseArnold.ProductLocal.exterior_dense line 285
  42. lemma OAI.MorseArnold.ProductLocal.exteriorField line 302
  43. lemma OAI.MorseArnold.ProductLocal.quadFlow_msmooth line 334
  44. lemma OAI.MorseArnold.ProductLocal.smooth_product_flow line 340
  45. lemma OAI.MorseArnold.ProductLocal.exterior_smooth line 354
  46. theorem OAI.MorseArnold.ProductLocal.zero_prod_toSpanSingleton line 361
  47. lemma OAI.MorseArnold.ProductLocal.exterior_integral line 370
  48. lemma OAI.MorseArnold.ProductLocal.exterior_no_fixed line 392
  49. theorem OAI.MorseArnold.ProductLocal.productLocalObligation line 400