OAI/Geometry/SplitTangent/RationalTrivialization.lean

GitHub source file

217 declarations, 0 contain sorry, 0 declared as axioms

Rational Trivialization.

  1. def OAI.SplitTangent.TangentSplitting.coordinateProjector line 23
  2. def OAI.SplitTangent.TangentSplitting.coordinateMatrix line 28
  3. theorem OAI.SplitTangent.TangentSplitting.coordinateMatrix_mulVec line 31
  4. theorem OAI.SplitTangent.TangentSplitting.coordinateProjector_idempotent line 35
  5. theorem OAI.SplitTangent.TangentSplitting.coordinateMatrix_idempotent line 44
  6. theorem OAI.SplitTangent.TangentSplitting.coordinateMatrix_analytic line 59
  7. def OAI.SplitTangent.TangentSplitting.coordinateTransition line 92
  8. theorem OAI.SplitTangent.TangentSplitting.coordinateTransition_analytic line 95
  9. theorem OAI.SplitTangent.TangentSplitting.coordinateTransition_derivative line 105
  10. theorem OAI.SplitTangent.TangentSplitting.coordinateProjector_intertwining line 135
  11. def OAI.SplitTangent.HolomorphicLinearODE.solutionCoeff line 168
  12. lemma OAI.SplitTangent.HolomorphicLinearODE.solutionCoeff_recurrence line 175
  13. lemma OAI.SplitTangent.HolomorphicLinearODE.solutionCoeff_norm line 183
  14. def OAI.SplitTangent.HolomorphicLinearODE.series line 212
  15. lemma OAI.SplitTangent.HolomorphicLinearODE.series_coeff line 216
  16. lemma OAI.SplitTangent.HolomorphicLinearODE.series_radius line 220
  17. lemma OAI.SplitTangent.HolomorphicLinearODE.solutionSeries_pos line 234
  18. lemma OAI.SplitTangent.HolomorphicLinearODE.cauchy_eval line 241
  19. lemma OAI.SplitTangent.HolomorphicLinearODE.hasDerivAt_solutionSeries line 252
  20. lemma OAI.SplitTangent.HolomorphicLinearODE.coeff_bound line 284
  21. lemma OAI.SplitTangent.HolomorphicLinearODE.series_of_coeff line 303
  22. lemma OAI.SplitTangent.HolomorphicLinearODE.exists_local_solution line 308
  23. lemma OAI.SplitTangent.HolomorphicLinearODE.inverse_mul_horizontal line 335
  24. lemma OAI.SplitTangent.HolomorphicLinearODE.exists_local_fundamental line 351
  25. lemma OAI.SplitTangent.HolomorphicLinearODE.local_uniqueness line 360
  26. def OAI.SplitTangent.HolomorphicLinearODE.transport line 385
  27. lemma OAI.SplitTangent.HolomorphicLinearODE.transport_self line 388
  28. lemma OAI.SplitTangent.HolomorphicLinearODE.transport_trans line 392
  29. lemma OAI.SplitTangent.HolomorphicLinearODE.transport_isUnit line 398
  30. lemma OAI.SplitTangent.HolomorphicLinearODE.transport_analyticAt line 404
  31. lemma OAI.SplitTangent.HolomorphicLinearODE.transport_hasDerivAt line 414
  32. theorem OAI.SplitTangent.HolomorphicLinearODE.exists_local_transport line 422
  33. theorem OAI.SplitTangent.HolomorphicLinearODE.eqOn_of_solution line 443
  34. lemma OAI.SplitTangent.HolomorphicLinearODE.gauge_hasDerivAt line 459
  35. lemma OAI.SplitTangent.HolomorphicLinearODE.intertwine_eventually line 468
  36. lemma OAI.SplitTangent.HolomorphicLinearODE.transport_intertwines line 482
  37. lemma OAI.SplitTangent.HolomorphicLinearODE.solutionCoeff_differentiableOn line 494
  38. def OAI.SplitTangent.HolomorphicLinearODE.parameterSolution line 512
  39. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_differentiableOn line 517
  40. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_analyticAt line 537
  41. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_zero line 548
  42. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_eq_series_sum line 556
  43. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_hasDerivAt line 561
  44. lemma OAI.SplitTangent.HolomorphicLinearODE.changeOriginSeries_norm_bound line 580
  45. lemma OAI.SplitTangent.HolomorphicLinearODE.changeOrigin_norm_bound line 597
  46. def OAI.SplitTangent.HolomorphicLinearODE.verticalCoeff line 632
  47. lemma OAI.SplitTangent.HolomorphicLinearODE.verticalCoeff_differentiableAt line 635
  48. lemma OAI.SplitTangent.HolomorphicLinearODE.verticalCoeff_bound line 647
  49. lemma OAI.SplitTangent.HolomorphicLinearODE.verticalCoeff_sum line 657
  50. lemma OAI.SplitTangent.HolomorphicLinearODE.analytic_coefficient_polydisk line 666
  51. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_continuousOn line 721
  52. lemma OAI.SplitTangent.HolomorphicLinearODE.parameterSolution_analyticAt_curves line 754
  53. lemma OAI.SplitTangent.HolomorphicLinearODE.exists_parameter_fundamental line 781
  54. theorem OAI.SplitTangent.HolomorphicLinearODE.exists_parameter_transport line 829
  55. lemma OAI.SplitTangent.HolomorphicLinearODE.idempotent_derivative line 860
  56. lemma OAI.SplitTangent.HolomorphicLinearODE.projector_derivative_sandwich line 866
  57. def OAI.SplitTangent.HolomorphicLinearODE.projectorODE line 875
  58. lemma OAI.SplitTangent.HolomorphicLinearODE.projectorODE_commutator line 879
  59. lemma OAI.SplitTangent.HolomorphicLinearODE.projectorODE_analyticAt line 894
  60. theorem OAI.SplitTangent.HolomorphicLinearODE.exists_local_projector_transport line 901
  61. def OAI.SplitTangent.ParameterProjector.verticalDerivative line 947
  62. lemma OAI.SplitTangent.ParameterProjector.hasDerivAt_vertical line 950
  63. lemma OAI.SplitTangent.ParameterProjector.verticalDerivative_analyticAt line 955
  64. def OAI.SplitTangent.ParameterProjector.equation line 960
  65. lemma OAI.SplitTangent.ParameterProjector.equation_analyticAt line 963
  66. lemma OAI.SplitTangent.ParameterProjector.equation_eq line 969
  67. lemma OAI.SplitTangent.ParameterProjector.exists_preserving_parameter_fundamental line 976
  68. lemma OAI.SplitTangent.ParameterProjector.exists_preserving_parameter_transport line 1035
  69. lemma OAI.SplitTangent.PullbackConnection.projected_bracket_eq line 1075
  70. def OAI.SplitTangent.PullbackConnection.coefficient line 1089
  71. def OAI.SplitTangent.PullbackConnection.covariantDerivative line 1093
  72. lemma OAI.SplitTangent.PullbackConnection.coefficient_analyticAt line 1096
  73. lemma OAI.SplitTangent.PullbackConnection.covariantDerivative_pulled_section line 1105
  74. lemma OAI.SplitTangent.PullbackConnection.covariantDerivative_leibniz line 1124
  75. def OAI.SplitTangent.PullbackConnection.equation line 1136
  76. lemma OAI.SplitTangent.PullbackConnection.equation_analyticAt line 1139
  77. lemma OAI.SplitTangent.PullbackConnection.projectorODE_horizontal line 1145
  78. lemma OAI.SplitTangent.PullbackConnection.horizontal_of_equation line 1159
  79. theorem OAI.SplitTangent.PullbackConnection.exists_local_horizontal_transport line 1171
  80. def OAI.SplitTangent.PullbackConnection.familyCoefficient line 1209
  81. lemma OAI.SplitTangent.PullbackConnection.familyCoefficient_analyticAt line 1212
  82. lemma OAI.SplitTangent.PullbackConnection.familyCoefficient_eq line 1224
  83. lemma OAI.SplitTangent.PullbackConnection.familyEquation_eq line 1232
  84. theorem OAI.SplitTangent.PullbackConnection.exists_horizontal_parameter_transport line 1241
  85. theorem OAI.SplitTangent.PullbackConnection.covariantDerivative_naturality line 1302
  86. lemma OAI.SplitTangent.HolomorphicLinearODE.inverse_apply_horizontal line 1357
  87. theorem OAI.SplitTangent.HolomorphicLinearODE.vector_local_uniqueness line 1376
  88. lemma OAI.SplitTangent.PullbackConnection.hasDerivAt_equation_of_horizontal line 1412
  89. lemma OAI.SplitTangent.PullbackConnection.horizontal_local_uniqueness line 1436
  90. theorem OAI.SplitTangent.PullbackConnection.horizontal_chart_compatibility line 1462
  91. theorem OAI.SplitTangent.PullbackConnection.horizontal_eqOn line 1507
  92. theorem OAI.SplitTangent.TwoChartCovering.exists_normalized_lifts line 1531
  93. structure OAI.SplitTangent.HorizontalCovering.HorizontalCocycle line 1566
  94. def OAI.SplitTangent.HorizontalCovering.HorizontalCocycle.toCore line 1583
  95. theorem OAI.SplitTangent.HorizontalCovering.HorizontalCocycle.isCoveringMap line 1600
  96. theorem OAI.SplitTangent.HorizontalCovering.HorizontalCocycle.coordinates_locally_constant line 1605
  97. theorem OAI.SplitTangent.HorizontalCovering.HorizontalCocycle.lift_local_form line 1620
  98. theorem OAI.SplitTangent.HorizontalCovering.HorizontalCocycle.exists_two_chart_lifts line 1641
  99. structure OAI.SplitTangent.HorizontalCovering.LocalTransportData line 1655
  100. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.localEquiv line 1670
  101. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.reverse_self line 1676
  102. theorem OAI.SplitTangent.HorizontalCovering.LocalTransportData.equiv_nonempty line 1682
  103. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.fiberEquiv line 1694
  104. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.toCocycle line 1699
  105. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.decode line 1725
  106. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.encode line 1728
  107. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.decode_encode line 1731
  108. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.decode_local_frame line 1735
  109. theorem OAI.SplitTangent.HorizontalCovering.LocalTransportData.decode_lift_local_form line 1744
  110. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.IsHorizontalAlong line 1763
  111. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.horizontal_local_form line 1767
  112. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.horizontal_base line 1773
  113. theorem OAI.SplitTangent.HorizontalCovering.LocalTransportData.horizontal_equalizer_clopen line 1780
  114. theorem OAI.SplitTangent.HorizontalCovering.LocalTransportData.horizontal_unique line 1806
  115. theorem OAI.SplitTangent.HorizontalCovering.LocalTransportData.exists_normalized_horizontal line 1817
  116. theorem OAI.SplitTangent.HorizontalCovering.LocalTransportData.exists_two_chart_horizontal line 1834
  117. abbrev OAI.SplitTangent.PullbackConnection.ImageFiber line 1863
  118. structure OAI.SplitTangent.PullbackConnection.LocalImages line 1868
  119. lemma OAI.SplitTangent.PullbackConnection.LocalImages.center line 1885
  120. lemma OAI.SplitTangent.PullbackConnection.LocalImages.trans_analytic line 1888
  121. def OAI.SplitTangent.PullbackConnection.LocalImages.forward line 1894
  122. def OAI.SplitTangent.PullbackConnection.LocalImages.reverse line 1900
  123. lemma OAI.SplitTangent.PullbackConnection.LocalImages.forward_val line 1907
  124. lemma OAI.SplitTangent.PullbackConnection.LocalImages.reverse_val line 1910
  125. lemma OAI.SplitTangent.PullbackConnection.LocalImages.left_inverse line 1914
  126. lemma OAI.SplitTangent.PullbackConnection.LocalImages.right_inverse line 1925
  127. lemma OAI.SplitTangent.PullbackConnection.LocalImages.normalized_forward line 1936
  128. lemma OAI.SplitTangent.PullbackConnection.LocalImages.overlap line 1941
  129. def OAI.SplitTangent.PullbackConnection.LocalImages.toData line 1969
  130. theorem OAI.SplitTangent.PullbackConnection.exists_local_images line 1986
  131. lemma OAI.SplitTangent.PullbackConnection.covariantDerivative_congr line 2000
  132. theorem OAI.SplitTangent.PullbackConnection.exists_entire_horizontal line 2006
  133. theorem OAI.SplitTangent.PullbackConnection.entire_horizontal_unique line 2040
  134. theorem OAI.SplitTangent.TangentSplitting.coordinateProjector_analytic line 2065
  135. lemma OAI.SplitTangent.TangentSplitting.coordinateProjector_fixed line 2086
  136. lemma OAI.SplitTangent.TangentSplitting.coordinateCurve_analytic line 2096
  137. lemma OAI.SplitTangent.TangentSplitting.coordinateCurve_derivative line 2104
  138. lemma OAI.SplitTangent.TangentSplitting.coordinateCurve_complementary line 2125
  139. lemma OAI.SplitTangent.TangentSplitting.coordinateProjector_eventually_idempotent line 2134
  140. theorem OAI.SplitTangent.TangentSplitting.exists_manifold_local_transport line 2144
  141. abbrev OAI.SplitTangent.TangentSplitting.TangentImageFiber line 2177
  142. structure OAI.SplitTangent.TangentSplitting.LocalChartImages line 2182
  143. abbrev OAI.SplitTangent.TangentSplitting.LocalChartImages.frame line 2201
  144. abbrev OAI.SplitTangent.TangentSplitting.LocalChartImages.coords line 2202
  145. abbrev OAI.SplitTangent.TangentSplitting.LocalChartImages.uncoords line 2203
  146. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.center line 2205
  147. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.frame_mem line 2206
  148. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.uncoords_coords line 2208
  149. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.coords_uncoords line 2210
  150. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.coords_fixed line 2213
  151. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.uncoords_fixed line 2217
  152. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.trans_analytic line 2228
  153. def OAI.SplitTangent.TangentSplitting.LocalChartImages.forward line 2234
  154. def OAI.SplitTangent.TangentSplitting.LocalChartImages.reverse line 2241
  155. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.forward_val line 2248
  156. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.reverse_val line 2251
  157. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.left_inverse line 2255
  158. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.right_inverse line 2267
  159. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.normalized_forward line 2279
  160. theorem OAI.SplitTangent.TangentSplitting.exists_local_chart_images line 2288
  161. lemma OAI.SplitTangent.PullbackConnection.covariantDerivative_curve_congr line 2298
  162. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.transition_curve line 2308
  163. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.transition_derivative line 2314
  164. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.overlap_locally_unique line 2324
  165. def OAI.SplitTangent.TangentSplitting.LocalChartImages.toData line 2412
  166. theorem OAI.SplitTangent.TangentSplitting.exists_manifold_horizontal line 2429
  167. theorem OAI.SplitTangent.AnalyticContinuation.subset_of_local_analytic_equations line 2485
  168. lemma OAI.SplitTangent.AnalyticManifoldMaps.equality_local_equations line 2518
  169. theorem OAI.SplitTangent.AnalyticManifoldMaps.eqOn_of_eventuallyEq line 2546
  170. lemma OAI.SplitTangent.PullbackConnection.covariantDerivative_reparam line 2561
  171. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.cover_section_coordinates line 2580
  172. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.cover_section_holomorphic line 2591
  173. lemma OAI.SplitTangent.TangentSplitting.rational_forward_germ line 2616
  174. lemma OAI.SplitTangent.rational_section_gluing line 2699
  175. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.horizontal_germ_of_value line 2748
  176. theorem OAI.SplitTangent.TangentSplitting.exists_rational_horizontal_section line 2763
  177. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalSection line 2822
  178. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalSection_horizontal line 2826
  179. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalSection_self line 2836
  180. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalSection_unique line 2842
  181. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalSection_cocycle line 2851
  182. def OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalTransport line 2857
  183. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalTransport_self line 2867
  184. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalTransport_cocycle line 2870
  185. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalTransport_germ line 2874
  186. def OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation line 2895
  187. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation_self line 2899
  188. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation_cocycle line 2903
  189. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation_holomorphic line 2907
  190. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation_add line 2913
  191. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation_smul line 2941
  192. def OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationLinear line 2978
  193. def OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap line 2988
  194. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_apply line 2996
  195. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_fixed line 3000
  196. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_self line 3004
  197. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_cocycle line 3010
  198. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_reverse line 3021
  199. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_holomorphic line 3025
  200. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalTransport_local line 3040
  201. lemma OAI.SplitTangent.HorizontalCovering.LocalTransportData.globalTransport_reverse_local line 3060
  202. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_reverse_local line 3077
  203. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_reverse_holomorphic_at line 3090
  204. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuation_germ line 3135
  205. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_apply_fixed line 3140
  206. lemma OAI.SplitTangent.TangentSplitting.rational_continuation_overlap line 3154
  207. lemma OAI.SplitTangent.holomorphic_const_fiber_linear_at line 3195
  208. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_source line 3225
  209. lemma OAI.SplitTangent.TangentSplitting.rational_reverse_overlap line 3234
  210. def OAI.SplitTangent.TangentSplitting.rationalReverseMap line 3270
  211. theorem OAI.SplitTangent.TangentSplitting.exists_rational_reverse_map line 3295
  212. lemma OAI.SplitTangent.holomorphic_along_sum_smul_at line 3312
  213. def OAI.SplitTangent.CurveBundleMap.ofSections line 3345
  214. lemma OAI.SplitTangent.CurveBundleMap.ofSections_finite line 3400
  215. lemma OAI.SplitTangent.CurveBundleMap.ofSections_infinity line 3415
  216. def OAI.SplitTangent.TangentSplitting.rationalContinuationSection line 3437
  217. theorem OAI.SplitTangent.TangentSplitting.exists_rational_trivialization line 3453