OAI/Geometry/ConjugatePoints/Coordinates.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThreeManifold.RiemannianCoordinates.chartBilin line 21
2. lemma OAI.ThreeManifold.RiemannianCoordinates.chartBilin_smoothAt line 24
3. lemma OAI.ThreeManifold.RiemannianCoordinates.matrix_smoothAt line 45
4. lemma OAI.ThreeManifold.RiemannianCoordinates.vector_expansion line 54
5. lemma OAI.ThreeManifold.RiemannianCoordinates.bilin_matrix line 58
6. lemma OAI.ThreeManifold.RiemannianCoordinates.matrix_posDef line 70
7. lemma OAI.ThreeManifold.RiemannianCoordinates.determinant_smoothAt line 93
8. lemma OAI.ThreeManifold.RiemannianCoordinates.adjugate_smoothAt line 100
9. lemma OAI.ThreeManifold.RiemannianCoordinates.inverse_smoothAt line 116
10. lemma OAI.ThreeManifold.RiemannianCoordinates.partial_smoothAt line 122
11. lemma OAI.ThreeManifold.RiemannianCoordinates.christoffel_smoothAt line 126
12. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureCoefficient_smoothAt line 140
13. lemma OAI.ThreeManifold.RiemannianCoordinates.matrix_symm line 153
14. lemma OAI.ThreeManifold.RiemannianCoordinates.matrix_partial_symm line 155
15. lemma OAI.ThreeManifold.RiemannianCoordinates.chartBilin_symm line 162
16. lemma OAI.ThreeManifold.RiemannianCoordinates.christoffel_symm line 164
17. lemma OAI.ThreeManifold.RiemannianCoordinates.lower_christoffel line 169
18. lemma OAI.ThreeManifold.RiemannianCoordinates.metric_coordinate_compatible line 194
19. lemma OAI.ThreeManifold.RiemannianCoordinates.fderiv_coordinate_expansion line 204
20. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_pairing line 209
21. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_pairing_right line 231
22. lemma OAI.ThreeManifold.RiemannianCoordinates.metric_directional_compatible line 251
23. def OAI.ThreeManifold.RiemannianCoordinates.connectionLinear line 271
24. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionLinear_apply line 275
25. def OAI.ThreeManifold.RiemannianCoordinates.curvatureLinear line 280
26. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureLinear_apply line 284
27. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_smoothAt line 297
28. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_smoothAt line 309
29. lemma OAI.ThreeManifold.RiemannianCoordinates.curve_coordinates_smoothAt line 321
30. lemma OAI.ThreeManifold.RiemannianCoordinates.along_smoothAt line 329
31. lemma OAI.ThreeManifold.RiemannianCoordinates.interval_enlargement line 336
32. lemma OAI.ThreeManifold.RiemannianCoordinates.linear_ode_zero_on line 345
33. def OAI.ThreeManifold.RiemannianCoordinates.jacobiBlock line 374
34. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobiBlock_apply line 377
35. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_zero_in_chart line 380
36. def OAI.ThreeManifold.RiemannianCoordinates.connectionBilin line 439
37. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionBilin_apply line 445
38. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionBilin_smoothAt line 455
39. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionBilin_deriv_apply line 465
40. lemma OAI.ThreeManifold.RiemannianCoordinates.deltaConnection_apply line 497
41. lemma OAI.ThreeManifold.RiemannianCoordinates.doubleConnection_apply line 514
42. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_connection line 535
43. lemma OAI.ThreeManifold.RiemannianCoordinates.metric_fields_hasDerivAt line 582
44. def OAI.ThreeManifold.RiemannianCoordinates.localIndexDensity line 617
45. def OAI.ThreeManifold.RiemannianCoordinates.localBoundary line 622
46. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_boundary_hasDerivAt line 626
47. lemma OAI.ThreeManifold.RiemannianCoordinates.transition_smoothAt line 664
48. lemma OAI.ThreeManifold.RiemannianCoordinates.overlap_nhds line 673
49. lemma OAI.ThreeManifold.RiemannianCoordinates.chart_metric_transform line 679
50. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionTerm_symm line 699
51. lemma OAI.ThreeManifold.RiemannianCoordinates.chartBilin_pos line 711
52. lemma OAI.ThreeManifold.RiemannianCoordinates.symmetric_skew_difference_zero line 720
53. lemma OAI.ThreeManifold.RiemannianCoordinates.transition_metric_derivative line 744
54. lemma OAI.ThreeManifold.RiemannianCoordinates.transition_derivative_surjective line 791
55. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_change line 801
56. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_change_derivative line 836
57. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_change line 888
58. lemma OAI.ThreeManifold.RiemannianCoordinates.along_change line 921
59. lemma OAI.ThreeManifold.RiemannianCoordinates.along_congr line 946
60. lemma OAI.ThreeManifold.RiemannianCoordinates.field_coordinates_change line 952
61. lemma OAI.ThreeManifold.RiemannianCoordinates.field_along_change line 971
62. structure OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry line 999
63. lemma OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry.smoothAt line 1014
64. lemma OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry.metric_derivative line 1016
65. lemma OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry.connection line 1061
66. lemma OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry.connection_derivative line 1100
67. lemma OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry.curvature line 1150
68. lemma OAI.ThreeManifold.RiemannianCoordinates.CoordinateMetricIsometry.along line 1180
69. structure OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry line 1210
70. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.smoothAt line 1220
71. def OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinateDomain line 1223
72. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinateDomain_open line 1226
73. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinate_smoothAt line 1235
74. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinate_metric line 1243
75. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinate_surjective line 1265
76. def OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinates line 1279
77. def OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative line 1295
78. lemma OAI.ThreeManifold.RiemannianCoordinates.push_from_chart line 1301
79. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_coordinates line 1315
80. lemma OAI.ThreeManifold.RiemannianCoordinates.metric_field_coordinates line 1327
81. def OAI.ThreeManifold.RiemannianCoordinates.SmoothFieldOn line 1343
82. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_smoothField line 1347
83. lemma OAI.ThreeManifold.RiemannianCoordinates.smoothField_coordinatesAt line 1351
84. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_smooth line 1360
85. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_mono line 1376
86. lemma OAI.ThreeManifold.RiemannianCoordinates.zero_germ_derivative line 1383
87. lemma OAI.ThreeManifold.RiemannianCoordinates.chart_interval line 1398
88. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_zero_of_initial line 1408
89. lemma OAI.ThreeManifold.RiemannianCoordinates.intrinsic_pairing_hasDerivAt line 1458
90. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_zero_of_intrinsic_initial line 1486
91. def OAI.ThreeManifold.RiemannianCoordinates.velocity line 1501
92. lemma OAI.ThreeManifold.RiemannianCoordinates.velocity_coordinates line 1504
93. lemma OAI.ThreeManifold.RiemannianCoordinates.velocity_smooth line 1515
94. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_acceleration_zero line 1525
95. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_speed_hasDerivAt line 1540
96. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_iterate_coordinates line 1547
97. def OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong line 1564
98. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_coordinates line 1570
99. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_smooth line 1592
100. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_intrinsic_equation line 1610
101. def OAI.ThreeManifold.RiemannianCoordinates.indexDensity line 1626
102. lemma OAI.ThreeManifold.RiemannianCoordinates.indexDensity_coordinates line 1631
103. lemma OAI.ThreeManifold.RiemannianCoordinates.fieldCoordinates_add line 1647
104. lemma OAI.ThreeManifold.RiemannianCoordinates.fieldCoordinates_smul line 1654
105. lemma OAI.ThreeManifold.RiemannianCoordinates.fieldCoordinates_zero line 1661
106. lemma OAI.ThreeManifold.RiemannianCoordinates.smoothField_add line 1667
107. lemma OAI.ThreeManifold.RiemannianCoordinates.smoothField_smul line 1674
108. lemma OAI.ThreeManifold.RiemannianCoordinates.smoothField_zero line 1682
109. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_add line 1686
110. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_smul line 1709
111. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_add line 1738
112. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_smul line 1750
113. lemma OAI.ThreeManifold.RiemannianCoordinates.intrinsic_pairing_smooth line 1761
114. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionBilin_symm line 1782
115. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionBilin_deriv_symm line 1785
116. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_skew line 1798
117. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_bianchi line 1803
118. lemma OAI.ThreeManifold.RiemannianCoordinates.bilin_derivative_compatible line 1831
119. lemma OAI.ThreeManifold.RiemannianCoordinates.bilin_derivative_line line 1851
120. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionBilin_line line 1873
121. lemma OAI.ThreeManifold.RiemannianCoordinates.bilin_connection_line line 1886
122. lemma OAI.ThreeManifold.RiemannianCoordinates.bilin_second_compatible line 1901
123. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_pairing_skew line 1927
124. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_pairing_selfAdjoint line 1941