OAI/Geometry/EinsteinFour/GeodesicGeometry13.lean

GitHub source file

207 declarations, 0 contain sorry, 0 declared as axioms

Real complex circles are exactly multiplication by unit complex scalars.

  1. def OAI.PositiveEinsteinFour.Geometry.complexPhase line 31
  2. theorem OAI.PositiveEinsteinFour.Geometry.complexPhase_norm line 33
  3. theorem OAI.PositiveEinsteinFour.Geometry.complexPhase_arg line 40
  4. theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_circle_standard line 51
  5. theorem OAI.PositiveEinsteinFour.Geometry.complexCircle_standard_of_phase line 59
  6. theorem OAI.PositiveEinsteinFour.Geometry.directionFrameMatrix_standard_complex line 80
  7. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameAction_direction_standard line 88
  8. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_direction_standard line 97
  9. def OAI.PositiveEinsteinFour.Geometry.complexPolarLift line 117
  10. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLift_norm line 122
  11. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLift_ne_zero line 138
  12. def OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar line 144
  13. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLift_inner line 147
  14. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_complexPolar line 163
  15. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_minimizing line 189
  16. theorem OAI.PositiveEinsteinFour.Geometry.complex_direction_injective line 211
  17. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_injOn_ball line 242
  18. theorem OAI.PositiveEinsteinFour.Geometry.cp2_exists_first_aligned line 288
  19. def OAI.PositiveEinsteinFour.Geometry.complexHeadTail line 328
  20. theorem OAI.PositiveEinsteinFour.Geometry.complexHeadTail_norm_sq line 331
  21. theorem OAI.PositiveEinsteinFour.Geometry.complexHeadTail_inner line 337
  22. theorem OAI.PositiveEinsteinFour.Geometry.complexPolar_angle_mem line 359
  23. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_radius_eq line 367
  24. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_interior_injective line 394
  25. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_first_standard line 440
  26. theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingTangentDomain_complex line 484
  27. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_closedBall_image line 506
  28. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_fiber_norm line 514
  29. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_interior_fiber line 523
  30. def OAI.PositiveEinsteinFour.Geometry.complexAffineLift line 546
  31. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLift_ne_zero line 549
  32. def OAI.PositiveEinsteinFour.Geometry.complexAffinePoint line 554
  33. theorem OAI.PositiveEinsteinFour.Geometry.complexAffinePoint_injective line 557
  34. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_affine line 570
  35. theorem OAI.PositiveEinsteinFour.Geometry.complex_diagonal_pairing line 616
  36. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_first_pairing line 627
  37. theorem OAI.PositiveEinsteinFour.Geometry.complexPolar_radius_angle line 660
  38. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLift_radius line 663
  39. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_boundary_phase line 668
  40. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_boundary_circle line 686
  41. theorem OAI.PositiveEinsteinFour.Geometry.exists_radial_direction line 706
  42. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_surjective line 716
  43. theorem OAI.PositiveEinsteinFour.Geometry.exists_complex_interior_coordinates line 793
  44. def OAI.PositiveEinsteinFour.Geometry.complexAffineRadius line 825
  45. def OAI.PositiveEinsteinFour.Geometry.complexAffineLog line 828
  46. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineRadius_mem line 831
  47. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLog_norm line 842
  48. theorem OAI.PositiveEinsteinFour.Geometry.complexAffinePoint_polar_log line 850
  49. def OAI.PositiveEinsteinFour.Geometry.complexCompanion line 889
  50. theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_companion line 892
  51. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_pairing line 903
  52. def OAI.PositiveEinsteinFour.Geometry.complexProjectiveNorth line 986
  53. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_zero line 988
  54. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_north_polar line 993
  55. def OAI.PositiveEinsteinFour.Geometry.complexProjectiveEvaluation line 1016
  56. def OAI.PositiveEinsteinFour.Geometry.complexProjectiveTopology line 1019
  57. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectiveEvaluation_injective line 1024
  58. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectiveEvaluation_isEmbedding line 1031
  59. theorem OAI.PositiveEinsteinFour.Geometry.complexProjective_t2Space line 1034
  60. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLift_continuous line 1037
  61. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectivePolar_continuous line 1050
  62. structure OAI.PositiveEinsteinFour.Geometry.ComplexProjectivePolarData line 1078
  63. def OAI.PositiveEinsteinFour.Geometry.complexProjectivePolarData line 1084
  64. def OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap line 1094
  65. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_eq_of_projective_polar_eq line 1099
  66. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_polar line 1126
  67. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLog_zero line 1155
  68. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineRadius_continuous line 1158
  69. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLog_continuous line 1161
  70. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_left_continuous line 1190
  71. theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_inner_re line 1211
  72. theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_inner_im line 1217
  73. theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_inner_norm_sq line 1224
  74. abbrev OAI.PositiveEinsteinFour.Geometry.ComplexPolarDomain line 1243
  75. def OAI.PositiveEinsteinFour.Geometry.complexPolarProjection line 1245
  76. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarProjection_surjective line 1248
  77. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarProjection_continuous line 1253
  78. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarProjection_isQuotientMap line 1262
  79. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_radial line 1285
  80. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_surjective line 1301
  81. theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_linear_norm_sq line 1345
  82. def OAI.PositiveEinsteinFour.Geometry.complexPolarLiftDifferential line 1353
  83. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLiftDifferential_norm_sq line 1360
  84. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_continuous line 1390
  85. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_distance_from_center line 1430
  86. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_fiber_eq_of_radial_lt line 1446
  87. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLift_headTail line 1491
  88. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLiftDifferential_inner line 1497
  89. theorem OAI.PositiveEinsteinFour.Geometry.complexPolarLiftDifferential_inner_norm_sq line 1509
  90. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_affine line 1533
  91. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_affine_continuous line 1549
  92. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_affine_injective line 1565
  93. def OAI.PositiveEinsteinFour.Geometry.complexNormalLift line 1595
  94. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalLift_radial line 1599
  95. theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_norm_radial line 1605
  96. theorem OAI.PositiveEinsteinFour.Geometry.complexHeadTail_hasDerivAt line 1617
  97. theorem OAI.PositiveEinsteinFour.Geometry.complex_projective_differential_gram line 1647
  98. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalLift_hasDerivAt line 1685
  99. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_metric_eq_horizontal line 1740
  100. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalLift_norm line 1771
  101. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalLift_ne_zero line 1783
  102. def OAI.PositiveEinsteinFour.Geometry.complexNormalPoint line 1789
  103. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalPoint_radial line 1792
  104. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_normal line 1802
  105. theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_curve_speed line 1842
  106. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineRadius_pos line 1888
  107. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLog_ne_zero line 1892
  108. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLog_differentiableAt line 1898
  109. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalPoint_affineLog line 1910
  110. def OAI.PositiveEinsteinFour.Geometry.complexHorizontalPart line 1927
  111. theorem OAI.PositiveEinsteinFour.Geometry.complexHorizontalPart_orthogonal line 1929
  112. theorem OAI.PositiveEinsteinFour.Geometry.complexHorizontalPart_norm_sq line 1933
  113. theorem OAI.PositiveEinsteinFour.Geometry.complexHorizontalPart_phase line 1943
  114. theorem OAI.PositiveEinsteinFour.Geometry.complexHorizontalPart_phase_norm line 1964
  115. def OAI.PositiveEinsteinFour.Geometry.complexGreatCircle line 1981
  116. def OAI.PositiveEinsteinFour.Geometry.complexGreatCircleVelocity line 1984
  117. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_hasDerivAt line 1987
  118. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_norm line 1991
  119. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircleVelocity_norm line 2002
  120. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_horizontal line 2013
  121. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_horizontal_speed line 2022
  122. theorem OAI.PositiveEinsteinFour.Geometry.complex_unit_aligned_coefficient line 2041
  123. theorem OAI.PositiveEinsteinFour.Geometry.complexHorizontalPart_curve_invariant line 2047
  124. theorem OAI.PositiveEinsteinFour.Geometry.complex_real_inner_mul_self line 2084
  125. theorem OAI.PositiveEinsteinFour.Geometry.complexHorizontalPairing line 2091
  126. theorem OAI.PositiveEinsteinFour.Geometry.complex_horizontal_inner_bound line 2101
  127. theorem OAI.PositiveEinsteinFour.Geometry.complex_unit_curve_tangent line 2111
  128. def OAI.PositiveEinsteinFour.Geometry.complexTailLinear line 2135
  129. def OAI.PositiveEinsteinFour.Geometry.complexTailCLM line 2140
  130. def OAI.PositiveEinsteinFour.Geometry.complexVectorAffine line 2143
  131. theorem OAI.PositiveEinsteinFour.Geometry.complexVectorAffine_differentiableAt line 2146
  132. theorem OAI.PositiveEinsteinFour.Geometry.complexAffinePoint_vector line 2152
  133. theorem OAI.PositiveEinsteinFour.Geometry.complexAffineLog_contDiffAt line 2175
  134. theorem OAI.PositiveEinsteinFour.Geometry.complexVectorAffine_contDiffAt line 2187
  135. def OAI.PositiveEinsteinFour.Geometry.complexGreatCircleUnit line 2207
  136. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_contDiff line 2211
  137. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircleUnit_continuous line 2215
  138. def OAI.PositiveEinsteinFour.Geometry.complexSphereProjection line 2232
  139. theorem OAI.PositiveEinsteinFour.Geometry.complexSphereProjection_continuous line 2235
  140. theorem OAI.PositiveEinsteinFour.Geometry.complexSphereProjection_affine line 2247
  141. theorem OAI.PositiveEinsteinFour.Geometry.complex_trigonometric_zeros_subsingleton line 2263
  142. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_coordinate_zeros_finite line 2291
  143. theorem OAI.PositiveEinsteinFour.Geometry.complex_aligned_circle line 2311
  144. theorem OAI.PositiveEinsteinFour.Geometry.complex_orthonormal_pair_tail line 2359
  145. theorem OAI.PositiveEinsteinFour.Geometry.complexVectorAffine_ne_zero_of_coordinate line 2384
  146. theorem OAI.PositiveEinsteinFour.Geometry.complexGreatCircle_regular_off_finite line 2396
  147. theorem OAI.PositiveEinsteinFour.Geometry.cp2UnitRep_coordinate_ne_zero_of_unit line 2425
  148. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_sphere_continuous line 2440
  149. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_unit_continuous line 2472
  150. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_lift_contMDiffAt line 2485
  151. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_lift_speed line 2538
  152. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_local_curve_lift line 2614
  153. theorem OAI.PositiveEinsteinFour.Geometry.complex_overlap_derivative_bound line 2690
  154. theorem OAI.PositiveEinsteinFour.Geometry.complex_angle_derivative_bound line 2726
  155. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_unit_le_chord line 2763
  156. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_greatCircle_distance_le line 2815
  157. def OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveSection line 2870
  158. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveSection_rightInverse line 2876
  159. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_section_germ line 2881
  160. theorem OAI.PositiveEinsteinFour.Geometry.complex_angle_curve_sub_le line 2915
  161. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_lift_curve_sub_le line 2936
  162. def OAI.PositiveEinsteinFour.Geometry.complexNormalize line 2967
  163. theorem OAI.PositiveEinsteinFour.Geometry.complexNormalize_projection line 2972
  164. theorem OAI.PositiveEinsteinFour.Geometry.complex_normalization_distance_le line 2977
  165. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_distance_le_of_affine line 3018
  166. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_inverse_angle_derivative line 3073
  167. theorem OAI.PositiveEinsteinFour.Geometry.complexProjective_compactSpace line 3134
  168. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_section_continuousAt line 3145
  169. def OAI.PositiveEinsteinFour.Geometry.complexCutLift line 3187
  170. theorem OAI.PositiveEinsteinFour.Geometry.complexCutLift_norm_ge_one line 3190
  171. theorem OAI.PositiveEinsteinFour.Geometry.complexCutLift_ne_zero line 3195
  172. def OAI.PositiveEinsteinFour.Geometry.complexCutPoint line 3198
  173. theorem OAI.PositiveEinsteinFour.Geometry.complexCutLift_sub_norm line 3201
  174. theorem OAI.PositiveEinsteinFour.Geometry.complexCutPoint_distance_le line 3209
  175. theorem OAI.PositiveEinsteinFour.Geometry.complexCutPoint_covers line 3222
  176. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_self line 3275
  177. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_comm line 3278
  178. theorem OAI.PositiveEinsteinFour.Geometry.fubiniStudyDistance_eq_zero_iff line 3282
  179. theorem OAI.PositiveEinsteinFour.Geometry.complexProjective_open_iff line 3288
  180. def OAI.PositiveEinsteinFour.Geometry.complexProjectiveMetric line 3317
  181. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_distance_le line 3340
  182. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_inverse_curve_sub_le line 3411
  183. def OAI.PositiveEinsteinFour.Geometry.complexProjectiveInterior line 3462
  184. theorem OAI.PositiveEinsteinFour.Geometry.complexProjectiveInterior_dense line 3465
  185. theorem OAI.PositiveEinsteinFour.Geometry.exists_complexInterior_sequence line 3480
  186. theorem OAI.PositiveEinsteinFour.Geometry.cp2Overlap_north line 3498
  187. theorem OAI.PositiveEinsteinFour.Geometry.cp2UnitRep_cut_head line 3507
  188. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjectiveMap_cut_iff line 3523
  189. theorem OAI.PositiveEinsteinFour.Geometry.actual_complex_cut_disk_cover line 3549
  190. theorem OAI.PositiveEinsteinFour.Geometry.actual_complex_cut_disk_distance_le line 3569
  191. def OAI.PositiveEinsteinFour.Geometry.complexParametrizedCone line 3596
  192. theorem OAI.PositiveEinsteinFour.Geometry.complexParametrizedCone_dimH_le line 3599
  193. theorem OAI.PositiveEinsteinFour.Geometry.complexParametrizedCone_hausdorff_four_zero line 3630
  194. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_inverse_interior_curve_le line 3656
  195. def OAI.PositiveEinsteinFour.Geometry.metricHausdorffThree line 3723
  196. theorem OAI.PositiveEinsteinFour.Geometry.actual_complex_cut_hausdorff_three_zero line 3730
  197. theorem OAI.PositiveEinsteinFour.Geometry.exists_not_mem_of_dimH_le_three line 3778
  198. theorem OAI.PositiveEinsteinFour.Geometry.segment_avoids_of_not_mem_complexCone line 3788
  199. theorem OAI.PositiveEinsteinFour.Geometry.exists_complexParametrized_detour line 3810
  200. theorem OAI.PositiveEinsteinFour.Geometry.complex_frameGeodesic_radial_distance line 3851
  201. theorem OAI.PositiveEinsteinFour.Geometry.complex_frameGeodesic_injOn line 3863
  202. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_inverse_interior_geodesic_le line 3873
  203. def OAI.PositiveEinsteinFour.Geometry.complexCutChartMap line 3921
  204. def OAI.PositiveEinsteinFour.Geometry.complexCutChartDomain line 3925
  205. theorem OAI.PositiveEinsteinFour.Geometry.complexCutChartMap_locallyLipschitz line 3930
  206. theorem OAI.PositiveEinsteinFour.Geometry.dist_le_of_segment_local_bound line 3970
  207. theorem OAI.PositiveEinsteinFour.Geometry.actualComplexProjective_section_local_distance line 4023