OAI/Geometry/ConjugatePoints/Metric.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

Pullback Riemannian metrics and smooth cylinder coordinates.

  1. abbrev OAI.ThreeManifold.MetricConstruction.Metric line 23
  2. def OAI.ThreeManifold.MetricConstruction.pullBilin line 27
  3. lemma OAI.ThreeManifold.MetricConstruction.pullBilin_apply line 30
  4. lemma OAI.ThreeManifold.MetricConstruction.flip_smoothAt line 33
  5. lemma OAI.ThreeManifold.MetricConstruction.bilin_comp_smoothAt line 52
  6. def OAI.ThreeManifold.MetricConstruction.pullInner line 62
  7. lemma OAI.ThreeManifold.MetricConstruction.pullInner_apply line 67
  8. lemma OAI.ThreeManifold.MetricConstruction.pullback_coordinates line 72
  9. lemma OAI.ThreeManifold.MetricConstruction.pullback_inner_smoothAt line 102
  10. lemma OAI.ThreeManifold.MetricConstruction.pullback_inner_smooth line 122
  11. lemma OAI.ThreeManifold.MetricConstruction.pullInner_comp line 133
  12. lemma OAI.ThreeManifold.MetricConstruction.pullInner_congr line 144
  13. def OAI.ThreeManifold.MetricConstruction.pullback line 151
  14. lemma OAI.ThreeManifold.MetricConstruction.covering_inverse_mdifferentiable line 191
  15. lemma OAI.ThreeManifold.MetricConstruction.inverse_pullInner_independent line 205
  16. def OAI.ThreeManifold.MetricConstruction.descendInner line 229
  17. lemma OAI.ThreeManifold.MetricConstruction.descendInner_eq line 233
  18. lemma OAI.ThreeManifold.MetricConstruction.descendInner_smooth line 243
  19. lemma OAI.ThreeManifold.MetricConstruction.descendInner_symm line 259
  20. lemma OAI.ThreeManifold.MetricConstruction.descendInner_pos line 266
  21. lemma OAI.ThreeManifold.MetricConstruction.descendInner_bounded line 281
  22. def OAI.ThreeManifold.MetricConstruction.descend line 293
  23. lemma OAI.ThreeManifold.MetricConstruction.descend_local line 300
  24. lemma OAI.ThreeManifold.MetricConstruction.descend_projection line 306
  25. lemma OAI.ThreeManifold.MetricConstruction.metric_nonneg line 338
  26. def OAI.ThreeManifold.MetricConstruction.scaleSq line 344
  27. def OAI.ThreeManifold.MetricConstruction.flatBilin line 367
  28. def OAI.ThreeManifold.MetricConstruction.euclideanInner line 369
  29. lemma OAI.ThreeManifold.MetricConstruction.euclidean_inner_smooth line 372
  30. def OAI.ThreeManifold.MetricConstruction.euclidean line 392
  31. lemma OAI.ThreeManifold.MetricConstruction.circle_action_deriv line 414
  32. lemma OAI.ThreeManifold.MetricConstruction.circle_action_invariant line 422
  33. def OAI.ThreeManifold.MetricConstruction.circle line 430
  34. lemma OAI.ThreeManifold.MetricConstruction.circle_projection line 435
  35. instance OAI.ThreeManifold.MetricConstruction.(instance at line 449) line 449
  36. instance OAI.ThreeManifold.MetricConstruction.(instance at line 451) line 451
  37. lemma OAI.ThreeManifold.MetricConstruction.projection_fst_smooth line 456
  38. lemma OAI.ThreeManifold.MetricConstruction.projection_snd_smooth line 460
  39. def OAI.ThreeManifold.MetricConstruction.productInner line 464
  40. lemma OAI.ThreeManifold.MetricConstruction.productInner_apply line 468
  41. lemma OAI.ThreeManifold.MetricConstruction.bilin_product_bounded line 481
  42. def OAI.ThreeManifold.MetricConstruction.product line 495
  43. def OAI.ThreeManifold.MetricConstruction.modelInner line 528
  44. lemma OAI.ThreeManifold.MetricConstruction.model_inner_smooth line 531
  45. def OAI.ThreeManifold.MetricConstruction.modelMetric line 551
  46. def OAI.ThreeManifold.MetricConstruction.piBilin line 562
  47. lemma OAI.ThreeManifold.MetricConstruction.piBilin_apply line 565
  48. lemma OAI.ThreeManifold.MetricConstruction.piBilin_symm line 567
  49. lemma OAI.ThreeManifold.MetricConstruction.piBilin_pos line 569
  50. lemma OAI.ThreeManifold.MetricConstruction.piBilin_bounded line 577
  51. lemma OAI.ThreeManifold.MetricConstruction.twistedPi_smooth line 589
  52. lemma OAI.ThreeManifold.MetricConstruction.twistedPi_bounded line 602
  53. def OAI.ThreeManifold.MetricConstruction.twistedPi line 608
  54. abbrev OAI.ThreeManifold.MetricConstruction.V3 line 618
  55. def OAI.ThreeManifold.MetricConstruction.triangular line 620
  56. lemma OAI.ThreeManifold.MetricConstruction.triangular_apply line 640
  57. lemma OAI.ThreeManifold.MetricConstruction.triangular_smooth line 643
  58. def OAI.ThreeManifold.MetricConstruction.triangularMetric line 656
  59. lemma OAI.ThreeManifold.MetricConstruction.triangularMetric_apply line 662
  60. lemma OAI.ThreeManifold.MetricConstruction.inverse_smooth_of_sections line 677
  61. abbrev OAI.ThreeManifold.CylinderConstruction.P line 704
  62. abbrev OAI.ThreeManifold.CylinderConstruction.Cylinder line 705
  63. abbrev OAI.ThreeManifold.CylinderConstruction.Deck line 706
  64. instance OAI.ThreeManifold.CylinderConstruction.identity_action line 707
  65. lemma OAI.ThreeManifold.CylinderConstruction.identity_cover line 711
  66. instance OAI.ThreeManifold.CylinderConstruction.torus_action line 720
  67. instance OAI.ThreeManifold.CylinderConstruction.cylinder_action line 722
  68. def OAI.ThreeManifold.CylinderConstruction.projection line 724
  69. lemma OAI.ThreeManifold.CylinderConstruction.projection_cover line 725
  70. lemma OAI.ThreeManifold.CylinderConstruction.projection_smooth line 729
  71. lemma OAI.ThreeManifold.CylinderConstruction.deck_formula line 741
  72. lemma OAI.ThreeManifold.CylinderConstruction.action_smooth line 752
  73. lemma OAI.ThreeManifold.CylinderConstruction.local_sections line 756
  74. lemma OAI.ThreeManifold.CylinderConstruction.local_inverse_smooth line 777
  75. def OAI.ThreeManifold.CylinderConstruction.coordinates line 783
  76. def OAI.ThreeManifold.CylinderConstruction.model line 791
  77. lemma OAI.ThreeManifold.CylinderConstruction.model_apply line 799
  78. lemma OAI.ThreeManifold.CylinderConstruction.deck_deriv line 812
  79. def OAI.ThreeManifold.CylinderConstruction.lifted line 821
  80. lemma OAI.ThreeManifold.CylinderConstruction.lifted_apply line 825
  81. lemma OAI.ThreeManifold.CylinderConstruction.lifted_invariant line 831
  82. def OAI.ThreeManifold.CylinderConstruction.sectionMap line 838
  83. lemma OAI.ThreeManifold.CylinderConstruction.section_spec line 840
  84. def OAI.ThreeManifold.CylinderConstruction.metric line 845
  85. lemma OAI.ThreeManifold.CylinderConstruction.metric_projection line 849
  86. def OAI.ThreeManifold.MetricConstruction.pullbackHomeomorph line 863
  87. lemma OAI.ThreeManifold.MetricConstruction.bilin_eq_of_pull_eq line 873
  88. def OAI.ThreeManifold.MetricConstruction.coveringDerivative line 890
  89. lemma OAI.ThreeManifold.MetricConstruction.coveringDerivative_eq line 895
  90. def OAI.ThreeManifold.MetricConstruction.liftedDerivative line 909
  91. lemma OAI.ThreeManifold.MetricConstruction.liftedDerivative_eq line 915
  92. def OAI.ThreeManifold.MetricConstruction.pullbackFromLift line 942
  93. lemma OAI.ThreeManifold.MetricConstruction.pull_composition line 958