OAI/Geometry/ConjugatePoints/Distance.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Riemannian distance and the nonpositively curved universal-cover metric.

  1. lemma OAI.ThreeManifold.RiemannianDistance.edist_finite_of_preconnected line 18
  2. abbrev OAI.ThreeManifold.RiemannianDistance.metricSpace line 42
  3. lemma OAI.ThreeManifold.RiemannianDistance.tangent_enorm line 49
  4. lemma OAI.ThreeManifold.RiemannianDistance.norm_sub_le_pathELength line 56
  5. lemma OAI.ThreeManifold.RiemannianDistance.norm_sub_le_riemannianEDist line 77
  6. lemma OAI.ThreeManifold.RiemannianDistance.norm_sub_le_dist line 91
  7. theorem OAI.ThreeManifold.RiemannianDistance.properSpace line 104
  8. lemma OAI.ThreeManifold.RiemannianDistance.pathELength_comp_eq line 121
  9. lemma OAI.ThreeManifold.RiemannianDistance.riemannianEDist_map_le line 146
  10. theorem OAI.ThreeManifold.RiemannianDistance.isometry_of_inner line 161
  11. lemma OAI.ThreeManifold.MetricConstruction.flip_contAt line 183
  12. lemma OAI.ThreeManifold.MetricConstruction.bilin_comp_contAt line 202
  13. lemma OAI.ThreeManifold.MetricConstruction.pullback_inner_contAt line 212
  14. def OAI.ThreeManifold.MetricConstruction.continuousPullback line 232
  15. def OAI.ThreeManifold.RiemannianCoordinates.exponentialTangentEquiv line 264
  16. def OAI.ThreeManifold.RiemannianCoordinates.exponentialMetric line 270
  17. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialMetric_inner line 275
  18. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialMetric_expanding line 281
  19. def OAI.ThreeManifold.UniversalDeck.group line 293
  20. instance OAI.ThreeManifold.UniversalDeck.deckAction line 304
  21. instance OAI.ThreeManifold.UniversalDeck.deckContinuous line 308
  22. lemma OAI.ThreeManifold.UniversalDeck.map_smul line 310
  23. lemma OAI.ThreeManifold.UniversalDeck.deck_ext line 314
  24. lemma OAI.ThreeManifold.UniversalDeck.covering_surjective line 321
  25. lemma OAI.ThreeManifold.UniversalDeck.exists_deck line 331
  26. theorem OAI.ThreeManifold.UniversalDeck.quotient_cover line 350
  27. def OAI.ThreeManifold.UniversalDeck.fundamentalGroupEquiv line 371
  28. lemma OAI.ThreeManifold.RiemannianCoordinates.lift_contDiff line 383
  29. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialDeck_contDiff line 401
  30. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialDeck_inner line 407
  31. lemma OAI.ThreeManifold.QuotientCoverGeometry.locallyFinite_graphs line 443
  32. theorem OAI.ThreeManifold.QuotientCoverGeometry.properlyDiscontinuous line 468
  33. theorem OAI.ThreeManifold.QuotientCoverGeometry.compact_fundamental_set line 475
  34. lemma OAI.ThreeManifold.NoNPC.conjugate_displacement line 506
  35. theorem OAI.ThreeManifold.NoNPC.displacement_attains_minimum line 510
  36. lemma OAI.ThreeManifold.NoNPC.attained_minimum_positive line 546
  37. lemma OAI.ThreeManifold.NoNPC.product_shift_constant line 554
  38. lemma OAI.ThreeManifold.NoNPC.zero_shift_pythagoras line 565
  39. theorem OAI.ThreeManifold.NoNPC.shear_orthogonality_impossible line 574
  40. theorem OAI.ThreeManifold.NoNPC.shear_pythagoras_impossible line 580
  41. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialMetric_coercive line 598
  42. abbrev OAI.ThreeManifold.RiemannianCoordinates.universalMetric line 616
  43. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_proper line 619
  44. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_deck_isometry line 624
  45. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_deck_displacement_minimum line 632
  46. lemma OAI.ThreeManifold.RiemannianDistance.pathELength_comp_eq_between line 660
  47. lemma OAI.ThreeManifold.RiemannianDistance.riemannianEDist_map_le_between line 687
  48. theorem OAI.ThreeManifold.RiemannianDistance.isometry_between line 704
  49. theorem OAI.ThreeManifold.UniversalCover.exists_based_homeomorph line 724
  50. lemma OAI.ThreeManifold.RiemannianCoordinates.lift_map_contDiff line 747
  51. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialChange_contDiff line 766
  52. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialChange_inner line 773
  53. theorem OAI.ThreeManifold.RiemannianCoordinates.exists_exponential_coordinates line 798
  54. lemma OAI.ThreeManifold.RiemannianDistance.functional_le_pathELength line 824
  55. lemma OAI.ThreeManifold.RiemannianDistance.functional_le_riemannianEDist line 849
  56. lemma OAI.ThreeManifold.RiemannianDistance.positive_bilinear_cauchy_schwarz line 861
  57. theorem OAI.ThreeManifold.RiemannianDistance.bilinear_le_riemannianEDist line 873
  58. lemma OAI.ThreeManifold.RiemannianCoordinates.globalGeodesic_speed line 917
  59. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialMetric_radial line 931
  60. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialMetric_radial_length line 961
  61. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_lower line 982
  62. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_radial_zero line 995
  63. lemma OAI.ThreeManifold.RiemannianCoordinates.exponential_recenter line 1020
  64. lemma OAI.ThreeManifold.RiemannianCoordinates.recenter_radial_line line 1030
  65. lemma OAI.ThreeManifold.RiemannianCoordinates.positive_form_smul line 1048
  66. lemma OAI.ThreeManifold.RiemannianCoordinates.positive_form_parallelogram line 1057
  67. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_lower_sq line 1067
  68. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_distance_zero_sq line 1076
  69. theorem OAI.ThreeManifold.RiemannianCoordinates.universalMetric_radial_CN line 1082