OAI/Geometry/ConjugatePoints/CompactMetric.lean

GitHub source file

196 declarations, 0 contain sorry, 0 declared as axioms

The smooth Riemannian metric on the compact glued manifold.

  1. def OAI.ThreeManifold.CompactMetric.radialLinear line 18
  2. def OAI.ThreeManifold.CompactMetric.radial line 41
  3. def OAI.ThreeManifold.CompactMetric.radialLift line 42
  4. lemma OAI.ThreeManifold.CompactMetric.radial_smooth line 43
  5. lemma OAI.ThreeManifold.CompactMetric.radialLift_smooth line 49
  6. lemma OAI.ThreeManifold.CompactMetric.radialLift_deriv line 51
  7. lemma OAI.ThreeManifold.CompactMetric.radial_commutes line 63
  8. def OAI.ThreeManifold.CompactMetric.radialPull line 65
  9. def OAI.ThreeManifold.CompactMetric.radius₁ line 72
  10. def OAI.ThreeManifold.CompactMetric.radius₂ line 73
  11. lemma OAI.ThreeManifold.CompactMetric.radius₁_smooth line 74
  12. lemma OAI.ThreeManifold.CompactMetric.radius₂_smooth line 76
  13. lemma OAI.ThreeManifold.CompactMetric.radius₁_pos line 78
  14. lemma OAI.ThreeManifold.CompactMetric.radius₂_pos line 80
  15. def OAI.ThreeManifold.CompactMetric.neck line 83
  16. lemma OAI.ThreeManifold.MetricConstruction.openSubtype_inverse_smooth line 94
  17. lemma OAI.ThreeManifold.MetricConstruction.openSubtype_mdifferentiable line 103
  18. def OAI.ThreeManifold.MetricConstruction.restrict line 111
  19. lemma OAI.ThreeManifold.MetricConstruction.restrict_inner line 115
  20. def OAI.ThreeManifold.CompactMetric.timeReverse line 123
  21. def OAI.ThreeManifold.CompactMetric.switch line 131
  22. lemma OAI.ThreeManifold.CompactMetric.switch_smooth line 132
  23. lemma OAI.ThreeManifold.CompactMetric.switch_symm_smooth line 142
  24. def OAI.ThreeManifold.CompactMetric.switched line 153
  25. abbrev OAI.ThreeManifold.CompactMetric.HeightCylinder line 156
  26. def OAI.ThreeManifold.CompactMetric.logDomain line 157
  27. def OAI.ThreeManifold.CompactMetric.logCylinderHomeomorph line 160
  28. lemma OAI.ThreeManifold.CompactMetric.logCylinder_smooth line 172
  29. lemma OAI.ThreeManifold.CompactMetric.logCylinder_symm_smooth line 184
  30. def OAI.ThreeManifold.CompactMetric.heightMetric line 197
  31. structure OAI.ThreeManifold.MetricConstruction.LocalMetric line 209
  32. def OAI.ThreeManifold.MetricConstruction.localGluedInner line 227
  33. lemma OAI.ThreeManifold.MetricConstruction.localGluedInner_eq line 230
  34. lemma OAI.ThreeManifold.MetricConstruction.localGluedInner_smooth line 235
  35. def OAI.ThreeManifold.MetricConstruction.glueLocal line 247
  36. lemma OAI.ThreeManifold.MetricConstruction.glueLocal_eq line 254
  37. def OAI.ThreeManifold.MetricConstruction.localPull line 265
  38. def OAI.ThreeManifold.MetricConstruction.localOn line 283
  39. abbrev OAI.ThreeManifold.CompactMetric.WholePiece line 296
  40. abbrev OAI.ThreeManifold.CompactMetric.EP line 297
  41. def OAI.ThreeManifold.CompactMetric.wholeCusp line 299
  42. def OAI.ThreeManifold.CompactMetric.wholeCoordinates line 302
  43. lemma OAI.ThreeManifold.CompactMetric.wholeCoordinates_smooth line 326
  44. lemma OAI.ThreeManifold.CompactMetric.wholeCoordinates_symm_smooth line 339
  45. lemma OAI.ThreeManifold.CompactMetric.wholeCusp_nonempty line 354
  46. def OAI.ThreeManifold.CompactMetric.cuspChart line 358
  47. lemma OAI.ThreeManifold.CompactMetric.cuspChart_smooth line 362
  48. lemma OAI.ThreeManifold.CompactMetric.cuspChart_mdifferentiable line 368
  49. def OAI.ThreeManifold.CompactMetric.cuspMetric line 374
  50. lemma OAI.ThreeManifold.MetricConstruction.halfPlane_coe_smooth line 389
  51. lemma OAI.ThreeManifold.MetricConstruction.halfPlane_coe_deriv line 395
  52. lemma OAI.ThreeManifold.MetricConstruction.halfPlane_im_smooth line 399
  53. def OAI.ThreeManifold.MetricConstruction.halfPlaneFlat line 402
  54. def OAI.ThreeManifold.MetricConstruction.hyperbolic line 406
  55. lemma OAI.ThreeManifold.MetricConstruction.hyperbolic_inner line 411
  56. lemma OAI.ThreeManifold.MetricConstruction.halfPlane_action_deriv line 418
  57. lemma OAI.ThreeManifold.MetricConstruction.halfPlane_action_deriv_apply line 434
  58. lemma OAI.ThreeManifold.MetricConstruction.hyperbolic_action_quadratic line 443
  59. lemma OAI.ThreeManifold.MetricConstruction.hyperbolic_action_invariant line 465
  60. lemma OAI.ThreeManifold.MetricConstruction.hyperbolic_effective_invariant line 479
  61. def OAI.ThreeManifold.MetricConstruction.surfaceHyperbolic line 484
  62. lemma OAI.ThreeManifold.MetricConstruction.surface_projection_isometry line 489
  63. lemma OAI.ThreeManifold.MetricConstruction.product_apply line 510
  64. lemma OAI.ThreeManifold.MetricConstruction.pull_product line 516
  65. lemma OAI.ThreeManifold.MetricConstruction.pull_scaleSq line 530
  66. abbrev OAI.ThreeManifold.CompactMetric.UniversalPiece line 542
  67. def OAI.ThreeManifold.CompactMetric.sourceProjection line 544
  68. lemma OAI.ThreeManifold.CompactMetric.sourceProjection_smooth line 546
  69. lemma OAI.ThreeManifold.CompactMetric.sourceProjection_deriv line 549
  70. lemma OAI.ThreeManifold.CompactMetric.sourceProjection_deriv_surjective line 556
  71. def OAI.ThreeManifold.CompactMetric.coreMetric line 571
  72. lemma OAI.ThreeManifold.CompactMetric.coreMetric_apply line 573
  73. lemma OAI.ThreeManifold.CompactMetric.coreMetric_projection line 578
  74. lemma OAI.ThreeManifold.MetricConstruction.pullbackFromLift_projection line 633
  75. def OAI.ThreeManifold.CompactMetric.heightToCylinder line 653
  76. lemma OAI.ThreeManifold.CompactMetric.heightToCylinder_smooth line 655
  77. lemma OAI.ThreeManifold.CompactMetric.heightMetric_inner line 658
  78. def OAI.ThreeManifold.CompactMetric.logCuspMap line 666
  79. lemma OAI.ThreeManifold.CompactMetric.logCuspMap_smoothAt line 668
  80. lemma OAI.ThreeManifold.CompactMetric.cuspMetric_inner line 673
  81. def OAI.ThreeManifold.CompactMetric.logarithmicLift line 684
  82. lemma OAI.ThreeManifold.CompactMetric.logarithmicLift_smooth line 685
  83. lemma OAI.ThreeManifold.CompactMetric.logCusp_projection_apply line 693
  84. lemma OAI.ThreeManifold.CompactMetric.logCusp_projection_germ line 707
  85. lemma OAI.ThreeManifold.CompactMetric.cuspMetric_projection line 714
  86. def OAI.ThreeManifold.CompactMetric.universalCoordinates line 735
  87. lemma OAI.ThreeManifold.CompactMetric.universalCoordinates_smooth line 736
  88. lemma OAI.ThreeManifold.CompactMetric.universalCoordinates_deriv line 738
  89. def OAI.ThreeManifold.CompactMetric.logLinear line 743
  90. lemma OAI.ThreeManifold.CompactMetric.logLinear_apply line 747
  91. def OAI.ThreeManifold.CompactMetric.logNormed line 749
  92. lemma OAI.ThreeManifold.CompactMetric.logNormed_deriv line 750
  93. lemma OAI.ThreeManifold.CompactMetric.logarithmicLift_deriv line 759
  94. def OAI.ThreeManifold.CompactMetric.period line 777
  95. def OAI.ThreeManifold.CompactMetric.leftLength line 778
  96. def OAI.ThreeManifold.CompactMetric.leftCircleScale line 780
  97. def OAI.ThreeManifold.CompactMetric.rightCircleScale line 781
  98. lemma OAI.ThreeManifold.CompactMetric.period_pos line 782
  99. lemma OAI.ThreeManifold.CompactMetric.leftCircleScale_pos line 784
  100. lemma OAI.ThreeManifold.CompactMetric.rightCircleScale_pos line 786
  101. lemma OAI.ThreeManifold.CompactMetric.leftLength_ge line 788
  102. lemma OAI.ThreeManifold.CompactMetric.exp_leftLength line 792
  103. lemma OAI.ThreeManifold.CompactMetric.ell_plateau line 796
  104. lemma OAI.ThreeManifold.CompactMetric.radius₁_left_exact line 800
  105. lemma OAI.ThreeManifold.CompactMetric.radius₂_left_exact line 810
  106. lemma OAI.ThreeManifold.CompactMetric.radius₂_right_exact line 815
  107. lemma OAI.ThreeManifold.CompactMetric.radius₁_right_exact line 825
  108. lemma OAI.ThreeManifold.CompactMetric.slope_left_exact line 830
  109. lemma OAI.ThreeManifold.CompactMetric.neck_projection_apply line 845
  110. lemma OAI.ThreeManifold.CompactMetric.radialPull_projection line 856
  111. def OAI.ThreeManifold.CompactMetric.switchLift line 869
  112. def OAI.ThreeManifold.CompactMetric.switchLinear line 870
  113. lemma OAI.ThreeManifold.CompactMetric.switchLift_eq line 877
  114. lemma OAI.ThreeManifold.CompactMetric.switchLift_smooth line 879
  115. lemma OAI.ThreeManifold.CompactMetric.switchLift_deriv line 883
  116. lemma OAI.ThreeManifold.CompactMetric.switch_commutes line 890
  117. lemma OAI.ThreeManifold.CompactMetric.switched_projection line 898
  118. def OAI.ThreeManifold.CompactMetric.leftCylinder line 908
  119. def OAI.ThreeManifold.CompactMetric.rightCylinder line 910
  120. lemma OAI.ThreeManifold.CompactMetric.leftCylinder_low line 913
  121. lemma OAI.ThreeManifold.CompactMetric.rightCylinder_low line 933
  122. lemma OAI.ThreeManifold.CompactMetric.cusp_linear_formula line 972
  123. lemma OAI.ThreeManifold.CompactMetric.cusp_core_match_projection line 985
  124. lemma OAI.ThreeManifold.CompactMetric.cusp_core_match line 997
  125. lemma OAI.ThreeManifold.CompactMetric.left_cusp_core_match line 1011
  126. lemma OAI.ThreeManifold.CompactMetric.right_cusp_core_match line 1016
  127. def OAI.ThreeManifold.CompactMetric.coreRegion line 1030
  128. def OAI.ThreeManifold.CompactMetric.cuspLevel line 1033
  129. lemma OAI.ThreeManifold.CompactMetric.cuspLevel_gt line 1034
  130. lemma OAI.ThreeManifold.CompactMetric.log_cuspLevel line 1037
  131. lemma OAI.ThreeManifold.CompactMetric.cuspMetric_domain line 1038
  132. def OAI.ThreeManifold.CompactMetric.wholeLocals line 1048
  133. lemma OAI.ThreeManifold.CompactMetric.wholeLocals_cover line 1050
  134. lemma OAI.ThreeManifold.CompactMetric.wholeLocals_compatible line 1061
  135. def OAI.ThreeManifold.CompactMetric.wholeMetric line 1080
  136. lemma OAI.ThreeManifold.CompactMetric.wholeMetric_core line 1082
  137. lemma OAI.ThreeManifold.CompactMetric.wholeMetric_cusp line 1085
  138. def OAI.ThreeManifold.CompactMetric.leftWhole line 1091
  139. def OAI.ThreeManifold.CompactMetric.rightWhole line 1093
  140. def OAI.ThreeManifold.CompactMetric.pieceMap line 1106
  141. lemma OAI.ThreeManifold.CompactMetric.pieceMap_smooth line 1107
  142. lemma OAI.ThreeManifold.CompactMetric.core8_nonempty line 1114
  143. def OAI.ThreeManifold.CompactMetric.pieceEmbedding line 1117
  144. lemma OAI.ThreeManifold.CompactMetric.pieceEmbedding_smooth_inverse line 1120
  145. lemma OAI.ThreeManifold.CompactMetric.pieceEmbedding_differentiable line 1127
  146. def OAI.ThreeManifold.CompactMetric.pieceMetric line 1133
  147. lemma OAI.ThreeManifold.CompactMetric.pieceMetric_inner line 1136
  148. def OAI.ThreeManifold.CompactMetric.leftPiece line 1139
  149. def OAI.ThreeManifold.CompactMetric.rightPiece line 1140
  150. lemma OAI.ThreeManifold.CompactMetric.cuspLevel_lt_two line 1145
  151. lemma OAI.ThreeManifold.CompactMetric.cuspMetric_change line 1150
  152. lemma OAI.ThreeManifold.CompactMetric.wholeMetric_cusp_two line 1167
  153. def OAI.ThreeManifold.CompactMetric.collarLog line 1184
  154. lemma OAI.ThreeManifold.CompactMetric.collarLog_smooth line 1185
  155. lemma OAI.ThreeManifold.CompactMetric.collarLog_eq line 1189
  156. lemma OAI.ThreeManifold.CompactMetric.pieceMetric_collar line 1199
  157. def OAI.ThreeManifold.CompactMetric.leftPosition line 1216
  158. def OAI.ThreeManifold.CompactMetric.rightPosition line 1217
  159. lemma OAI.ThreeManifold.CompactMetric.leftPosition_smooth line 1218
  160. lemma OAI.ThreeManifold.CompactMetric.rightPosition_smooth line 1220
  161. lemma OAI.ThreeManifold.CompactMetric.position_match line 1222
  162. lemma OAI.ThreeManifold.CompactMetric.leftPiece_collar line 1240
  163. lemma OAI.ThreeManifold.CompactMetric.rightPiece_collar line 1251
  164. lemma OAI.ThreeManifold.CompactMetric.gluing_smooth_self line 1276
  165. lemma OAI.ThreeManifold.CompactMetric.transition_smooth line 1278
  166. lemma OAI.ThreeManifold.CompactMetric.collar_pull_match line 1282
  167. lemma OAI.ThreeManifold.CompactMetric.piece_overlap line 1290
  168. def OAI.ThreeManifold.MetricConstruction.gluedInner line 1319
  169. lemma OAI.ThreeManifold.MetricConstruction.gluedInner_eq line 1324
  170. lemma OAI.ThreeManifold.MetricConstruction.gluedInner_smooth line 1329
  171. lemma OAI.ThreeManifold.MetricConstruction.gluedInner_symm line 1343
  172. lemma OAI.ThreeManifold.MetricConstruction.gluedInner_pos line 1349
  173. lemma OAI.ThreeManifold.MetricConstruction.gluedInner_bounded line 1357
  174. def OAI.ThreeManifold.MetricConstruction.glue line 1366
  175. lemma OAI.ThreeManifold.MetricConstruction.glue_local line 1373
  176. lemma OAI.ThreeManifold.MetricConstruction.glue_inverse line 1377
  177. abbrev OAI.ThreeManifold.GluedConstruction.EPm line 1403
  178. lemma OAI.ThreeManifold.GluedConstruction.inclusion_smooth line 1405
  179. def OAI.ThreeManifold.GluedConstruction.pieceOpenMap line 1421
  180. lemma OAI.ThreeManifold.GluedConstruction.pieceOpenMap_apply line 1423
  181. lemma OAI.ThreeManifold.GluedConstruction.pieceOpenMap_inclusion line 1424
  182. lemma OAI.ThreeManifold.GluedConstruction.pieceOpenMap_inverse_smooth line 1427
  183. lemma OAI.ThreeManifold.GluedConstruction.pieceOpenMap_mdifferentiable line 1447
  184. lemma OAI.ThreeManifold.GluedConstruction.pieceOpenMap_cover line 1453
  185. lemma OAI.ThreeManifold.CompactMetric.piece_inverse_transition line 1463
  186. lemma OAI.ThreeManifold.CompactMetric.piece_inverse_transition_germ line 1473
  187. lemma OAI.ThreeManifold.CompactMetric.glued_mixed_metric line 1481
  188. def OAI.ThreeManifold.CompactMetric.pieceMetrics line 1493
  189. lemma OAI.ThreeManifold.CompactMetric.pieceMetrics_compatible line 1495
  190. lemma OAI.ThreeManifold.CompactMetric.inverse_piece_smooth line 1505
  191. def OAI.ThreeManifold.CompactMetric.compactMetric line 1509
  192. lemma OAI.ThreeManifold.CompactMetric.compactMetric_local line 1512
  193. lemma OAI.ThreeManifold.Rechart.identity_smooth_forward line 1525
  194. lemma OAI.ThreeManifold.Rechart.identity_smooth_backward line 1545
  195. def OAI.ThreeManifold.CompactMetric.realCompactMetric line 1573
  196. theorem OAI.ThreeManifold.CompactMetric.closed_oriented_metric line 1578