OAI/Geometry/ConjugatePoints/Cometric.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

Radial profiles, cometrics, and collar estimates.

  1. def OAI.ThreeManifold.RadialProfile.cut line 16
  2. def OAI.ThreeManifold.RadialProfile.coordinate line 17
  3. def OAI.ThreeManifold.RadialProfile.slope line 19
  4. lemma OAI.ThreeManifold.RadialProfile.cut_smooth line 22
  5. lemma OAI.ThreeManifold.RadialProfile.cut_zero line 24
  6. lemma OAI.ThreeManifold.RadialProfile.cut_one line 26
  7. lemma OAI.ThreeManifold.RadialProfile.cut_nonneg line 28
  8. lemma OAI.ThreeManifold.RadialProfile.cut_le_one line 29
  9. lemma OAI.ThreeManifold.RadialProfile.cut_mono line 30
  10. lemma OAI.ThreeManifold.RadialProfile.cut_deriv_nonneg line 32
  11. lemma OAI.ThreeManifold.RadialProfile.cut_deriv_eq_zero line 33
  12. lemma OAI.ThreeManifold.RadialProfile.log_bounds line 45
  13. lemma OAI.ThreeManifold.RadialProfile.coordinate_smooth line 57
  14. lemma OAI.ThreeManifold.RadialProfile.coordinate_deriv line 60
  15. lemma OAI.ThreeManifold.RadialProfile.coordinate_left line 68
  16. lemma OAI.ThreeManifold.RadialProfile.coordinate_right line 70
  17. lemma OAI.ThreeManifold.RadialProfile.transition_difference_pos line 73
  18. lemma OAI.ThreeManifold.RadialProfile.slope_pos line 80
  19. lemma OAI.ThreeManifold.RadialProfile.coordinate_strictMono line 94
  20. lemma OAI.ThreeManifold.RadialProfile.coordinate_neck line 100
  21. lemma OAI.ThreeManifold.RadialProfile.coordinate_flip line 106
  22. def OAI.ThreeManifold.Cometric.a line 126
  23. def OAI.ThreeManifold.Cometric.A line 128
  24. def OAI.ThreeManifold.Cometric.χ line 130
  25. lemma OAI.ThreeManifold.Cometric.a_formula line 132
  26. lemma OAI.ThreeManifold.Cometric.a_smooth line 138
  27. lemma OAI.ThreeManifold.Cometric.a_nonneg line 141
  28. lemma OAI.ThreeManifold.Cometric.a_pos line 143
  29. lemma OAI.ThreeManifold.Cometric.a_eq_zero line 146
  30. lemma OAI.ThreeManifold.Cometric.a_lt_one line 149
  31. lemma OAI.ThreeManifold.Cometric.a_antitone line 155
  32. lemma OAI.ThreeManifold.Cometric.a_zero line 159
  33. lemma OAI.ThreeManifold.Cometric.a_eighth_ratio line 161
  34. lemma OAI.ThreeManifold.Cometric.a_hasDerivAt line 168
  35. lemma OAI.ThreeManifold.Cometric.a_deriv line 177
  36. lemma OAI.ThreeManifold.Cometric.a_deriv_nonpos line 180
  37. lemma OAI.ThreeManifold.Cometric.a_sq_le_neg_deriv line 184
  38. lemma OAI.ThreeManifold.Cometric.sq_le_exp line 200
  39. lemma OAI.ThreeManifold.Cometric.a_deriv_abs_le_one line 208
  40. lemma OAI.ThreeManifold.Cometric.neg_a_deriv_hasDerivAt line 219
  41. lemma OAI.ThreeManifold.Cometric.neg_a_deriv_antitone_mid line 234
  42. lemma OAI.ThreeManifold.Cometric.a_slope_lower line 248
  43. lemma OAI.ThreeManifold.Cometric.A_hasDerivAt line 259
  44. lemma OAI.ThreeManifold.Cometric.A_deriv line 262
  45. lemma OAI.ThreeManifold.Cometric.A_smooth line 264
  46. lemma OAI.ThreeManifold.Cometric.A_zero line 268
  47. lemma OAI.ThreeManifold.Cometric.A_nonneg line 270
  48. lemma OAI.ThreeManifold.Cometric.A_le line 273
  49. lemma OAI.ThreeManifold.Cometric.A_plateau line 279
  50. lemma OAI.ThreeManifold.Cometric.χ_smooth line 292
  51. lemma OAI.ThreeManifold.Cometric.χ_nonneg line 295
  52. lemma OAI.ThreeManifold.Cometric.χ_le_one line 296
  53. lemma OAI.ThreeManifold.Cometric.χ_monotone line 298
  54. lemma OAI.ThreeManifold.Cometric.χ_eq_zero line 302
  55. lemma OAI.ThreeManifold.Cometric.χ_eq_one line 305
  56. lemma OAI.ThreeManifold.Cometric.χ_eventually_zero line 308
  57. lemma OAI.ThreeManifold.Cometric.χ_eventually_one line 313
  58. lemma OAI.ThreeManifold.Cometric.χ_deriv_left line 318
  59. lemma OAI.ThreeManifold.Cometric.χ_deriv_right line 321
  60. lemma OAI.ThreeManifold.Cometric.χ_deriv2_left line 324
  61. lemma OAI.ThreeManifold.Cometric.χ_deriv2_right line 327
  62. lemma OAI.ThreeManifold.Cometric.χ_deriv_smooth line 330
  63. lemma OAI.ThreeManifold.Cometric.χ_deriv2_smooth line 333
  64. lemma OAI.ThreeManifold.Cometric.χ_derivative_bounds line 336
  65. def OAI.ThreeManifold.Collar.lam line 367
  66. lemma OAI.ThreeManifold.Collar.lam_smooth line 368
  67. lemma OAI.ThreeManifold.Collar.lam_nonneg line 369
  68. lemma OAI.ThreeManifold.Collar.lam_le_one line 370
  69. lemma OAI.ThreeManifold.Collar.lam_monotone line 371
  70. lemma OAI.ThreeManifold.Collar.lam_zero line 372
  71. lemma OAI.ThreeManifold.Collar.lam_one line 374
  72. lemma OAI.ThreeManifold.Collar.A_le_zero line 376
  73. lemma OAI.ThreeManifold.Collar.A_ge_self line 380
  74. lemma OAI.ThreeManifold.Collar.A_ge_neg_one line 387
  75. def OAI.ThreeManifold.Collar.denom line 392
  76. def OAI.ThreeManifold.Collar.rate line 393
  77. def OAI.ThreeManifold.Collar.k line 394
  78. def OAI.ThreeManifold.Collar.ell line 395
  79. lemma OAI.ThreeManifold.Collar.denom_lower line 397
  80. lemma OAI.ThreeManifold.Collar.denom_pos line 401
  81. lemma OAI.ThreeManifold.Collar.denom_smooth line 403
  82. lemma OAI.ThreeManifold.Collar.denom_hasDerivAt line 405
  83. lemma OAI.ThreeManifold.Collar.rate_contDiffAt line 407
  84. lemma OAI.ThreeManifold.Collar.rate_pos line 412
  85. lemma OAI.ThreeManifold.Collar.rate_le_delta line 416
  86. lemma OAI.ThreeManifold.Collar.k_eq_one line 422
  87. lemma OAI.ThreeManifold.Collar.k_eq_rate line 424
  88. lemma OAI.ThreeManifold.Collar.k_smooth line 426
  89. lemma OAI.ThreeManifold.Collar.k_positive line 436
  90. lemma OAI.ThreeManifold.Collar.rate_hasDerivAt line 445
  91. lemma OAI.ThreeManifold.Collar.rate_deriv_neg line 453
  92. lemma OAI.ThreeManifold.Collar.k_hasDerivAt line 462
  93. lemma OAI.ThreeManifold.Collar.k_deriv_nonpos line 476
  94. lemma OAI.ThreeManifold.Collar.ell_pos line 484
  95. lemma OAI.ThreeManifold.Collar.ell_zero line 485
  96. lemma OAI.ThreeManifold.Collar.integral_k_smooth line 486
  97. lemma OAI.ThreeManifold.Collar.ell_smooth line 493
  98. lemma OAI.ThreeManifold.Collar.ell_hasDerivAt line 495
  99. lemma OAI.ThreeManifold.Collar.ell_deriv line 501
  100. lemma OAI.ThreeManifold.Collar.ell_second line 504
  101. lemma OAI.ThreeManifold.Collar.ell_strictConvex_second line 511
  102. lemma OAI.ThreeManifold.Collar.squared_end_hasDerivAt line 519
  103. lemma OAI.ThreeManifold.Collar.squared_end_constant line 527
  104. lemma OAI.ThreeManifold.Collar.ell_end_germ line 535
  105. lemma OAI.ThreeManifold.Collar.ell_cusp_germ line 547
  106. theorem OAI.ThreeManifold.Collar.exact_convex_collar line 564