OAI/Geometry/Symplectic/MorseBounds/SphereCaps.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MorseArnold.SphereCaps.R3 line 13
  2. abbrev OAI.MorseArnold.SphereCaps.S2 line 14
  3. abbrev OAI.MorseArnold.SphereCaps.Plane line 15
  4. def OAI.MorseArnold.SphereCaps.vec3 line 18
  5. def OAI.MorseArnold.SphereCaps.radiusSq line 19
  6. def OAI.MorseArnold.SphereCaps.north line 20
  7. def OAI.MorseArnold.SphereCaps.south line 23
  8. def OAI.MorseArnold.SphereCaps.northInvAmbient line 26
  9. def OAI.MorseArnold.SphereCaps.southInvAmbient line 30
  10. def OAI.MorseArnold.SphereCaps.standardArea line 35
  11. lemma OAI.MorseArnold.SphereCaps.vec3_apply_zero line 40
  12. lemma OAI.MorseArnold.SphereCaps.vec3_apply_one line 41
  13. lemma OAI.MorseArnold.SphereCaps.vec3_apply_two line 42
  14. lemma OAI.MorseArnold.SphereCaps.sphere_equation line 43
  15. lemma OAI.MorseArnold.SphereCaps.height_bounds line 51
  16. lemma OAI.MorseArnold.SphereCaps.radiusSq_nonneg line 55
  17. lemma OAI.MorseArnold.SphereCaps.north_radius line 59
  18. lemma OAI.MorseArnold.SphereCaps.south_radius line 70
  19. lemma OAI.MorseArnold.SphereCaps.northInv_mem line 81
  20. lemma OAI.MorseArnold.SphereCaps.sqrt_pair line 96
  21. lemma OAI.MorseArnold.SphereCaps.north_left_inv line 102
  22. lemma OAI.MorseArnold.SphereCaps.northInv_height line 126
  23. lemma OAI.MorseArnold.SphereCaps.north_right_inv line 132
  24. lemma OAI.MorseArnold.SphereCaps.smooth_north line 157
  25. lemma OAI.MorseArnold.SphereCaps.smooth_northInvAmbient line 172
  26. lemma OAI.MorseArnold.SphereCaps.northPole_mem line 184
  27. def OAI.MorseArnold.SphereCaps.northInv line 188
  28. lemma OAI.MorseArnold.SphereCaps.northInv_val line 192
  29. lemma OAI.MorseArnold.SphereCaps.capDomain_open line 196
  30. def OAI.MorseArnold.SphereCaps.capDomain line 199
  31. lemma OAI.MorseArnold.SphereCaps.smooth_northInv line 201
  32. lemma OAI.MorseArnold.SphereCaps.north_map line 219
  33. def OAI.MorseArnold.SphereCaps.northChart line 224
  34. theorem OAI.MorseArnold.SphereCaps.north_chart line 248
  35. theorem OAI.MorseArnold.SphereCaps.caps_disjoint line 261
  36. def OAI.MorseArnold.SphereCaps.radialL line 272
  37. lemma OAI.MorseArnold.SphereCaps.radialL_apply line 275
  38. lemma OAI.MorseArnold.SphereCaps.radiusSq_deriv line 277
  39. lemma OAI.MorseArnold.SphereCaps.div_const_deriv line 285
  40. def OAI.MorseArnold.SphereCaps.vecL line 290
  41. lemma OAI.MorseArnold.SphereCaps.vecL_apply line 294
  42. lemma OAI.MorseArnold.SphereCaps.vec3_deriv line 299
  43. def OAI.MorseArnold.SphereCaps.northJac line 312
  44. theorem OAI.MorseArnold.SphereCaps.northInv_deriv line 320
  45. lemma OAI.MorseArnold.SphereCaps.area_northJac line 345
  46. def OAI.MorseArnold.SphereCaps.flipL line 367
  47. lemma OAI.MorseArnold.SphereCaps.flipL_apply line 372
  48. lemma OAI.MorseArnold.SphereCaps.flipL_involutive line 376
  49. lemma OAI.MorseArnold.SphereCaps.flipL_mem line 381
  50. def OAI.MorseArnold.SphereCaps.flipS line 391
  51. lemma OAI.MorseArnold.SphereCaps.flipS_involutive line 393
  52. lemma OAI.MorseArnold.SphereCaps.flipS_smooth line 397
  53. lemma OAI.MorseArnold.SphereCaps.north_flipS line 401
  54. lemma OAI.MorseArnold.SphereCaps.flip_northInv line 404
  55. lemma OAI.MorseArnold.SphereCaps.smooth_south line 409
  56. lemma OAI.MorseArnold.SphereCaps.south_map line 417
  57. def OAI.MorseArnold.SphereCaps.southChart line 422
  58. theorem OAI.MorseArnold.SphereCaps.south_chart line 458
  59. lemma OAI.MorseArnold.SphereCaps.standardArea_flip line 474
  60. lemma OAI.MorseArnold.SphereCaps.southInv_deriv line 479
  61. theorem OAI.MorseArnold.SphereCaps.cap_area line 484