OAI/Geometry/SplitTangent/FormalBoxes.lean

GitHub source file

706 declarations, 0 contain sorry, 0 declared as axioms

Formal Boxes.

  1. def OAI.SplitTangent.FormalCauchy.Causal line 24
  2. def OAI.SplitTangent.FormalCauchy.coefficients line 29
  3. theorem OAI.SplitTangent.FormalCauchy.coefficients_zero line 35
  4. theorem OAI.SplitTangent.FormalCauchy.coefficients_succ line 38
  5. theorem OAI.SplitTangent.FormalCauchy.existsUnique_coefficients line 48
  6. def OAI.SplitTangent.FormalCauchy.Agree line 70
  7. theorem OAI.SplitTangent.FormalCauchy.Agree.refl line 73
  8. theorem OAI.SplitTangent.FormalCauchy.Agree.mul line 75
  9. theorem OAI.SplitTangent.FormalCauchy.Agree.pow line 84
  10. theorem OAI.SplitTangent.FormalCauchy.Agree.prod line 90
  11. theorem OAI.SplitTangent.FormalCauchy.Agree.sum line 101
  12. theorem OAI.SplitTangent.FormalCauchy.Agree.subst line 110
  13. def OAI.SplitTangent.FormalCauchy.series line 130
  14. def OAI.SplitTangent.FormalCauchy.tailSeries line 134
  15. theorem OAI.SplitTangent.FormalCauchy.tailSeries_hasSubst line 138
  16. def OAI.SplitTangent.FormalCauchy.coefficientwise line 147
  17. def OAI.SplitTangent.FormalCauchy.rhs line 152
  18. def OAI.SplitTangent.FormalCauchy.operator line 156
  19. theorem OAI.SplitTangent.FormalCauchy.operator_causal line 161
  20. theorem OAI.SplitTangent.FormalCauchy.existsUnique_formalCoefficients line 175
  21. theorem OAI.SplitTangent.FormalCauchy.tailSeries_eq_sub line 184
  22. def OAI.SplitTangent.FormalCauchy.IsSolution line 193
  23. theorem OAI.SplitTangent.FormalCauchy.isSolution_series_iff line 200
  24. theorem OAI.SplitTangent.FormalCauchy.existsUnique_solution line 235
  25. def OAI.SplitTangent.FormalCauchy.analyticAlgebra line 256
  26. abbrev OAI.SplitTangent.FormalCauchy.AnalyticFunction line 264
  27. instance OAI.SplitTangent.FormalCauchy.(instance at line 266) line 266
  28. def OAI.SplitTangent.FormalCauchy.analyticDerivative line 270
  29. theorem OAI.SplitTangent.FormalCauchy.analyticDerivative_apply line 298
  30. theorem OAI.SplitTangent.FormalCauchy.analyticDerivative_mul line 303
  31. theorem OAI.SplitTangent.FormalCauchy.existsUnique_holomorphic_solution line 321
  32. def OAI.SplitTangent.FormalCauchy.analyticEvaluation line 330
  33. theorem OAI.SplitTangent.FormalCauchy.analyticEvaluation_apply line 333
  34. theorem OAI.SplitTangent.FormalCauchy.analyticDerivative_eqOn line 338
  35. theorem OAI.SplitTangent.FormalCauchy.operator_eqOn line 351
  36. theorem OAI.SplitTangent.FormalCauchy.holomorphic_coefficients_eqOn line 399
  37. theorem OAI.SplitTangent.FormalCauchy.polynomial_chain_rule line 439
  38. theorem OAI.SplitTangent.FormalCauchy.continuous_formal_pderiv line 458
  39. theorem OAI.SplitTangent.FormalCauchy.formal_chain_rule line 471
  40. def OAI.SplitTangent.FormalCauchy.deriveCoefficients line 499
  41. theorem OAI.SplitTangent.FormalCauchy.coeff_deriveCoefficients line 502
  42. def OAI.SplitTangent.FormalCauchy.coefficientDerivation line 505
  43. theorem OAI.SplitTangent.FormalCauchy.coefficientDerivation_apply line 530
  44. theorem OAI.SplitTangent.FormalCauchy.deriveCoefficients_C line 533
  45. theorem OAI.SplitTangent.FormalCauchy.deriveCoefficients_X line 541
  46. theorem OAI.SplitTangent.FormalCauchy.deriveCoefficients_add line 547
  47. theorem OAI.SplitTangent.FormalCauchy.deriveCoefficients_mul line 551
  48. theorem OAI.SplitTangent.FormalCauchy.continuous_deriveCoefficients line 560
  49. theorem OAI.SplitTangent.FormalCauchy.polynomial_coefficient_chain_rule line 569
  50. theorem OAI.SplitTangent.FormalCauchy.formal_coefficient_chain_rule line 598
  51. theorem OAI.SplitTangent.DiagonalRationality.iteratedDeriv_zero_of_growth line 635
  52. def OAI.SplitTangent.DiagonalRationality.taylorPolynomial line 655
  53. theorem OAI.SplitTangent.DiagonalRationality.eq_taylorPolynomial_of_growth line 658
  54. theorem OAI.SplitTangent.DiagonalRationality.degree_taylorPolynomial line 668
  55. def OAI.SplitTangent.DiagonalRationality.lineSections line 682
  56. theorem OAI.SplitTangent.DiagonalRationality.lineSections_growth line 701
  57. theorem OAI.SplitTangent.DiagonalRationality.lineSections_ext line 716
  58. theorem OAI.SplitTangent.DiagonalRationality.lineSections_eq_zero_of_neg line 732
  59. def OAI.SplitTangent.DiagonalRationality.sectionJet line 756
  60. theorem OAI.SplitTangent.DiagonalRationality.sectionJet_injective line 765
  61. instance OAI.SplitTangent.DiagonalRationality.lineSections_finite line 780
  62. theorem OAI.SplitTangent.DiagonalRationality.finrank_lineSections_le line 789
  63. def OAI.SplitTangent.DiagonalRationality.reciprocalNormal line 804
  64. theorem OAI.SplitTangent.DiagonalRationality.reciprocalNormal_constant line 807
  65. theorem OAI.SplitTangent.DiagonalRationality.reciprocalNormal_hasSubst line 811
  66. theorem OAI.SplitTangent.DiagonalRationality.reciprocalNormal_linear line 814
  67. theorem OAI.SplitTangent.DiagonalRationality.constant_subst line 822
  68. theorem OAI.SplitTangent.DiagonalRationality.leading_subst line 831
  69. def OAI.SplitTangent.DiagonalRationality.evaluateCoefficients line 850
  70. theorem OAI.SplitTangent.DiagonalRationality.coeff_evaluateCoefficients line 853
  71. def OAI.SplitTangent.DiagonalRationality.formalSections line 858
  72. def OAI.SplitTangent.DiagonalRationality.orderFiltration line 892
  73. def OAI.SplitTangent.DiagonalRationality.leadingSection line 906
  74. theorem OAI.SplitTangent.DiagonalRationality.leadingSection_eq_zero_iff line 929
  75. def OAI.SplitTangent.DiagonalRationality.leadingKernelEquiv line 947
  76. theorem OAI.SplitTangent.DiagonalRationality.orderFiltration_eq_zero line 964
  77. theorem OAI.SplitTangent.DiagonalRationality.finite_of_kernel line 983
  78. theorem OAI.SplitTangent.DiagonalRationality.filtration_dimension_bound line 992
  79. def OAI.SplitTangent.DiagonalRationality.zeroFiltrationEquiv line 1028
  80. theorem OAI.SplitTangent.DiagonalRationality.sum_descending_odds line 1037
  81. theorem OAI.SplitTangent.DiagonalRationality.formalSections_dimension_bound line 1051
  82. theorem OAI.SplitTangent.DiagonalRationality.twice_polynomial_dimension_gt line 1069
  83. def OAI.SplitTangent.DiagonalRationality.entireSeries line 1073
  84. theorem OAI.SplitTangent.DiagonalRationality.C_mem_entireSeries line 1087
  85. theorem OAI.SplitTangent.DiagonalRationality.X_mem_entireSeries line 1094
  86. def OAI.SplitTangent.DiagonalRationality.twistTransition line 1100
  87. theorem OAI.SplitTangent.DiagonalRationality.twistTransition_constant line 1103
  88. abbrev OAI.SplitTangent.DiagonalRationality.BiCoefficients line 1107
  89. def OAI.SplitTangent.DiagonalRationality.normalPolynomialSection line 1109
  90. def OAI.SplitTangent.DiagonalRationality.infinityPolynomialSection line 1112
  91. theorem OAI.SplitTangent.DiagonalRationality.normalPolynomialSection_entire line 1115
  92. theorem OAI.SplitTangent.DiagonalRationality.infinityPolynomialSection_entire line 1125
  93. theorem OAI.SplitTangent.DiagonalRationality.evaluateCoefficients_C line 1135
  94. theorem OAI.SplitTangent.DiagonalRationality.evaluateCoefficients_X line 1139
  95. theorem OAI.SplitTangent.DiagonalRationality.cancel_complementary_powers line 1143
  96. theorem OAI.SplitTangent.DiagonalRationality.polynomialSection_gluing line 1152
  97. def OAI.SplitTangent.DiagonalRationality.polynomialFunction line 1184
  98. theorem OAI.SplitTangent.DiagonalRationality.polynomialFunction_apply line 1187
  99. theorem OAI.SplitTangent.DiagonalRationality.polynomialFunction_injective line 1190
  100. def OAI.SplitTangent.DiagonalRationality.biPolynomial line 1194
  101. theorem OAI.SplitTangent.DiagonalRationality.biPolynomial_coeff line 1197
  102. theorem OAI.SplitTangent.DiagonalRationality.biPolynomial_injective line 1202
  103. def OAI.SplitTangent.DiagonalRationality.expandPolynomial line 1207
  104. theorem OAI.SplitTangent.DiagonalRationality.expandPolynomial_injective line 1210
  105. theorem OAI.SplitTangent.DiagonalRationality.polynomial_coe_sum line 1219
  106. theorem OAI.SplitTangent.DiagonalRationality.normalPolynomialSection_eq_expand line 1224
  107. theorem OAI.SplitTangent.DiagonalRationality.normalPolynomialSection_injective line 1240
  108. theorem OAI.SplitTangent.DiagonalRationality.C_complex_smul line 1246
  109. def OAI.SplitTangent.DiagonalRationality.chartPolynomialLinear line 1251
  110. theorem OAI.SplitTangent.DiagonalRationality.normalPolynomialSection_eq_linear line 1261
  111. theorem OAI.SplitTangent.DiagonalRationality.infinityPolynomialSection_eq_linear line 1270
  112. def OAI.SplitTangent.DiagonalRationality.polynomialSection line 1281
  113. theorem OAI.SplitTangent.DiagonalRationality.polynomialSection_injective line 1300
  114. def OAI.SplitTangent.DiagonalRationality.multiplySection line 1305
  115. def OAI.SplitTangent.DiagonalRationality.relationMap line 1318
  116. theorem OAI.SplitTangent.DiagonalRationality.finrank_biCoefficients line 1330
  117. theorem OAI.SplitTangent.DiagonalRationality.exists_polynomial_relation line 1333
  118. theorem OAI.SplitTangent.DiagonalRationality.entireSeries_cancel line 1363
  119. theorem OAI.SplitTangent.DiagonalRationality.exists_rational_relation line 1388
  120. theorem OAI.SplitTangent.DiagonalRationality.entireSeries_vanishing_of_mul line 1411
  121. def OAI.SplitTangent.DiagonalRationality.normalPolynomial line 1434
  122. theorem OAI.SplitTangent.DiagonalRationality.normalPolynomial_coe line 1438
  123. theorem OAI.SplitTangent.DiagonalRationality.cancel_normal_order line 1443
  124. theorem OAI.SplitTangent.DiagonalRationality.exists_reduced_polynomial_relation line 1468
  125. theorem OAI.SplitTangent.DiagonalRationality.exists_common_nonzero line 1505
  126. def OAI.SplitTangent.DiagonalRationality.polynomialEvaluation line 1519
  127. theorem OAI.SplitTangent.DiagonalRationality.polynomialEvaluation_diagonal line 1522
  128. theorem OAI.SplitTangent.DiagonalRationality.polynomialEvaluation_analytic line 1526
  129. theorem OAI.SplitTangent.DiagonalRationality.polynomial_quotient_analytic line 1542
  130. def OAI.SplitTangent.DiagonalRationality.taylorSeries line 1550
  131. theorem OAI.SplitTangent.DiagonalRationality.coeff_taylorSeries line 1553
  132. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_congr line 1557
  133. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_zero line 1563
  134. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_add line 1567
  135. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_mul line 1573
  136. theorem OAI.SplitTangent.DiagonalRationality.hasFPowerSeries_taylorSeries line 1589
  137. theorem OAI.SplitTangent.DiagonalRationality.polynomial_analyticAt line 1594
  138. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_polynomial line 1598
  139. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_quotient_relation line 1617
  140. theorem OAI.SplitTangent.DiagonalRationality.taylorSeries_quotient_eq line 1638
  141. theorem OAI.SplitTangent.DiagonalRationality.hasFPowerSeries_formal_quotient line 1661
  142. def OAI.SplitTangent.DiagonalRationality.polynomialFiber line 1673
  143. theorem OAI.SplitTangent.DiagonalRationality.polynomialFiber_coeff line 1676
  144. theorem OAI.SplitTangent.DiagonalRationality.polynomialFiber_eval line 1680
  145. theorem OAI.SplitTangent.DiagonalRationality.evaluateCoefficients_polynomial line 1684
  146. theorem OAI.SplitTangent.DiagonalRationality.reduced_relation_converges line 1692
  147. theorem OAI.SplitTangent.DiagonalRationality.exists_convergent_rational_quotient line 1710
  148. theorem OAI.SplitTangent.DiagonalRationality.exists_common_nonzero_finset line 1751
  149. theorem OAI.SplitTangent.DiagonalRationality.simultaneous_rational_reconstruction line 1779
  150. def OAI.SplitTangent.FormalProjective.AnalyticSeriesAt line 1816
  151. theorem OAI.SplitTangent.FormalProjective.AnalyticSeriesAt.add line 1823
  152. theorem OAI.SplitTangent.FormalProjective.AnalyticSeriesAt.mul line 1829
  153. theorem OAI.SplitTangent.FormalProjective.AnalyticSeriesAt.constant line 1835
  154. theorem OAI.SplitTangent.FormalProjective.AnalyticSeriesAt.sum line 1843
  155. theorem OAI.SplitTangent.FormalProjective.AnalyticSeriesAt.inv line 1850
  156. structure OAI.SplitTangent.FormalProjective.ChartData line 1880
  157. def OAI.SplitTangent.FormalProjective.ChartData.frame line 1896
  158. theorem OAI.SplitTangent.FormalProjective.ChartData.frame_constant line 1900
  159. theorem OAI.SplitTangent.FormalProjective.ChartData.frame_unit line 1908
  160. theorem OAI.SplitTangent.FormalProjective.ChartData.frame_analytic line 1913
  161. theorem OAI.SplitTangent.FormalProjective.ChartData.frame_overlap line 1921
  162. def OAI.SplitTangent.FormalProjective.ChartData.localSection line 1929
  163. theorem OAI.SplitTangent.FormalProjective.ChartData.frame_mul_localSection line 1933
  164. theorem OAI.SplitTangent.FormalProjective.ChartData.localSection_overlap line 1938
  165. theorem OAI.SplitTangent.FormalProjective.ChartData.localSection_constant line 1950
  166. theorem OAI.SplitTangent.FormalProjective.ChartData.localSection_analytic line 1957
  167. def OAI.SplitTangent.FormalProjective.ChartData.active line 1963
  168. theorem OAI.SplitTangent.FormalProjective.ChartData.active_nonzero line 1965
  169. def OAI.SplitTangent.FormalProjective.ChartData.sectionValue line 1968
  170. theorem OAI.SplitTangent.FormalProjective.ChartData.sectionValue_eq line 1971
  171. theorem OAI.SplitTangent.FormalProjective.ChartData.sectionValue_analytic line 1976
  172. theorem OAI.SplitTangent.FormalProjective.ChartData.sectionValue_constant line 1986
  173. def OAI.SplitTangent.FormalProjective.ChartData.sectionSeries line 1992
  174. theorem OAI.SplitTangent.FormalProjective.ChartData.sectionSeries_entire line 1996
  175. structure OAI.SplitTangent.FormalProjective.TwoChartData line 2008
  176. theorem OAI.SplitTangent.FormalProjective.TwoChartData.infinity_nonzero line 2021
  177. def OAI.SplitTangent.FormalProjective.TwoChartData.normalizedTransition line 2028
  178. theorem OAI.SplitTangent.FormalProjective.TwoChartData.normalizedTransition_constant line 2033
  179. theorem OAI.SplitTangent.FormalProjective.TwoChartData.sectionSeries_evaluate line 2046
  180. theorem OAI.SplitTangent.FormalProjective.TwoChartData.normalized_gluing line 2053
  181. def OAI.SplitTangent.FormalProjective.TwoChartData.normalizedSection line 2071
  182. theorem OAI.SplitTangent.FormalProjective.TwoChartData.normalizedSection_constant line 2077
  183. theorem OAI.SplitTangent.FormalProjective.ChartData.sectionValue_ratio line 2093
  184. theorem OAI.SplitTangent.DiagonalRationality.simultaneous_reconstruction_on_diagonal_patch line 2109
  185. theorem OAI.SplitTangent.FormalProjective.reconstruct_projective_map line 2154
  186. def OAI.SplitTangent.HolomorphicJets.normalDeriv line 2196
  187. def OAI.SplitTangent.HolomorphicJets.normalIterate line 2199
  188. theorem OAI.SplitTangent.HolomorphicJets.normalDeriv_analytic line 2203
  189. theorem OAI.SplitTangent.HolomorphicJets.normalIterate_analytic line 2207
  190. theorem OAI.SplitTangent.HolomorphicJets.normalDeriv_eq line 2213
  191. theorem OAI.SplitTangent.HolomorphicJets.normalIterate_eq line 2220
  192. theorem OAI.SplitTangent.HolomorphicJets.normalCoefficient_analytic line 2237
  193. def OAI.SplitTangent.HolomorphicJets.jetPolynomial line 2253
  194. theorem OAI.SplitTangent.HolomorphicJets.jetPolynomial_zero line 2257
  195. theorem OAI.SplitTangent.HolomorphicJets.jetPolynomial_congr line 2267
  196. def OAI.SplitTangent.HolomorphicJets.composeCoefficient line 2276
  197. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_causal line 2280
  198. theorem OAI.SplitTangent.HolomorphicJets.jetPolynomial_analytic line 2287
  199. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_analytic line 2300
  200. def OAI.SplitTangent.HolomorphicJets.jetSeries line 2318
  201. theorem OAI.SplitTangent.HolomorphicJets.jetSeries_apply line 2322
  202. def OAI.SplitTangent.HolomorphicJets.polynomialJet line 2327
  203. theorem OAI.SplitTangent.HolomorphicJets.polynomialJet_coeff line 2331
  204. theorem OAI.SplitTangent.HolomorphicJets.polynomialJet_eval line 2338
  205. theorem OAI.SplitTangent.HolomorphicJets.jetPolynomial_hasSeries line 2342
  206. theorem OAI.SplitTangent.HolomorphicJets.formalComposition_causal line 2352
  207. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_eq_formal line 2368
  208. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_eq_laterJet line 2390
  209. def OAI.SplitTangent.HolomorphicJets.composeJet line 2416
  210. theorem OAI.SplitTangent.HolomorphicJets.composeJet_zero line 2421
  211. theorem OAI.SplitTangent.HolomorphicJets.composeJet_eq_formal line 2428
  212. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_assoc line 2454
  213. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_deriv line 2472
  214. def OAI.SplitTangent.HolomorphicJets.directionDeriv line 2483
  215. theorem OAI.SplitTangent.HolomorphicJets.directionDeriv_analytic line 2486
  216. theorem OAI.SplitTangent.HolomorphicJets.directionDeriv_comm line 2493
  217. theorem OAI.SplitTangent.HolomorphicJets.directionDeriv_congr line 2502
  218. theorem OAI.SplitTangent.HolomorphicJets.normalIterate_directionDeriv line 2507
  219. def OAI.SplitTangent.HolomorphicJets.tangentDeriv line 2522
  220. theorem OAI.SplitTangent.HolomorphicJets.tangentDeriv_eq line 2524
  221. theorem OAI.SplitTangent.HolomorphicJets.deriv_normalCoefficient line 2532
  222. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_zero line 2553
  223. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_coordinate line 2558
  224. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_add line 2565
  225. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_mul line 2576
  226. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_sum line 2596
  227. def OAI.SplitTangent.HolomorphicJets.analyticJet line 2616
  228. theorem OAI.SplitTangent.HolomorphicJets.analyticJet_zero line 2620
  229. theorem OAI.SplitTangent.HolomorphicJets.analyticJet_hasSeries line 2624
  230. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_analyticJet line 2632
  231. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_sum line 2645
  232. def OAI.SplitTangent.HolomorphicJets.coordinatePartial line 2659
  233. theorem OAI.SplitTangent.HolomorphicJets.partial_analytic line 2662
  234. theorem OAI.SplitTangent.HolomorphicJets.linearMap_eq_sum line 2666
  235. theorem OAI.SplitTangent.HolomorphicJets.deriv_comp_eq_sum line 2676
  236. theorem OAI.SplitTangent.HolomorphicJets.taylor_deriv_comp line 2684
  237. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_normal_chain line 2709
  238. theorem OAI.SplitTangent.HolomorphicJets.tangentDeriv_comp line 2742
  239. theorem OAI.SplitTangent.HolomorphicJets.taylor_tangent_comp line 2758
  240. theorem OAI.SplitTangent.HolomorphicJets.composeCoefficient_tangent_chain line 2792
  241. def OAI.SplitTangent.HolomorphicJets.formalSubst line 2829
  242. theorem OAI.SplitTangent.HolomorphicJets.coeff_formalSubst line 2833
  243. theorem OAI.SplitTangent.HolomorphicJets.formalSubst_congr line 2837
  244. theorem OAI.SplitTangent.HolomorphicJets.formalSubst_mul line 2846
  245. theorem OAI.SplitTangent.HolomorphicJets.formalSubst_sum line 2855
  246. theorem OAI.SplitTangent.HolomorphicJets.formalSubst_assoc line 2862
  247. def OAI.SplitTangent.HolomorphicJets.normalVector line 2870
  248. def OAI.SplitTangent.HolomorphicJets.tangentVector line 2874
  249. def OAI.SplitTangent.HolomorphicJets.substitutedJacobian line 2878
  250. theorem OAI.SplitTangent.HolomorphicJets.normalVector_compose line 2882
  251. theorem OAI.SplitTangent.HolomorphicJets.tangentVector_compose line 2899
  252. def OAI.SplitTangent.HolomorphicJets.substitutedMatrix line 2918
  253. theorem OAI.SplitTangent.HolomorphicJets.substituted_intertwining line 2924
  254. theorem OAI.SplitTangent.HolomorphicJets.cauchy_target_covariance line 2955
  255. theorem OAI.SplitTangent.HolomorphicJets.formalComposition_outer_causal line 2979
  256. theorem OAI.SplitTangent.HolomorphicJets.coeff_subst_trunc line 2993
  257. theorem OAI.SplitTangent.HolomorphicJets.coeff_subst_congr line 3005
  258. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_const line 3017
  259. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_polynomial_comp line 3021
  260. theorem OAI.SplitTangent.HolomorphicJets.coeff_taylor_comp_trunc line 3044
  261. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_comp_zero line 3076
  262. def OAI.SplitTangent.HolomorphicJets.reparamJet line 3091
  263. theorem OAI.SplitTangent.HolomorphicJets.reparamJet_zero line 3095
  264. theorem OAI.SplitTangent.HolomorphicJets.reparamJet_eq_analyticJet line 3104
  265. theorem OAI.SplitTangent.HolomorphicJets.formalSubst_reparam line 3125
  266. def OAI.SplitTangent.FormalCauchy.analyticDerivation line 3156
  267. def OAI.SplitTangent.FormalCauchy.dCoeff line 3168
  268. theorem OAI.SplitTangent.FormalCauchy.coeff_dCoeff line 3172
  269. theorem OAI.SplitTangent.FormalCauchy.dCoeff_subst line 3177
  270. theorem OAI.SplitTangent.FormalCauchy.coeff_eval_dCoeff line 3185
  271. theorem OAI.SplitTangent.FormalCauchy.eval_dCoeff_subst line 3193
  272. def OAI.SplitTangent.FormalCauchy.analyticPullback line 3214
  273. theorem OAI.SplitTangent.FormalCauchy.eval_dCoeff_pullback line 3226
  274. def OAI.SplitTangent.HolomorphicJets.sourceDifference line 3246
  275. def OAI.SplitTangent.HolomorphicJets.sourceNormal line 3248
  276. theorem OAI.SplitTangent.HolomorphicJets.sourceDifference_analytic line 3251
  277. theorem OAI.SplitTangent.HolomorphicJets.sourceNormal_constant line 3258
  278. def OAI.SplitTangent.HolomorphicJets.sourceNormalFamily line 3265
  279. theorem OAI.SplitTangent.HolomorphicJets.sourceNormalFamily_eval line 3271
  280. theorem OAI.SplitTangent.HolomorphicJets.sourceNormalFamily_hasSubst line 3277
  281. theorem OAI.SplitTangent.HolomorphicJets.sourceDifference_tangent line 3287
  282. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_sub line 3301
  283. theorem OAI.SplitTangent.HolomorphicJets.eval_dCoeff_sourceNormal line 3309
  284. theorem OAI.SplitTangent.HolomorphicJets.substitutedMatrix_idempotent line 3348
  285. theorem OAI.SplitTangent.HolomorphicJets.projector_source_identity line 3364
  286. def OAI.SplitTangent.HolomorphicJets.sourceTransform line 3376
  287. theorem OAI.SplitTangent.HolomorphicJets.eval_pullback line 3383
  288. theorem OAI.SplitTangent.HolomorphicJets.eval_sourceTransform line 3393
  289. theorem OAI.SplitTangent.HolomorphicJets.normal_sourceTransform line 3409
  290. theorem OAI.SplitTangent.HolomorphicJets.tangent_sourceTransform line 3420
  291. theorem OAI.SplitTangent.HolomorphicJets.substitutedMatrix_sourceTransform line 3439
  292. theorem OAI.SplitTangent.HolomorphicJets.cauchy_source_covariance line 3471
  293. def OAI.SplitTangent.ActualCauchy.seed line 3523
  294. theorem OAI.SplitTangent.ActualCauchy.seed_zero line 3527
  295. theorem OAI.SplitTangent.ActualCauchy.seed_eq line 3531
  296. def OAI.SplitTangent.ActualCauchy.actualComposition line 3538
  297. theorem OAI.SplitTangent.ActualCauchy.actualComposition_apply line 3547
  298. theorem OAI.SplitTangent.ActualCauchy.actualComposition_causal line 3553
  299. def OAI.SplitTangent.ActualCauchy.actualOperator line 3567
  300. theorem OAI.SplitTangent.ActualCauchy.actualOperator_causal line 3574
  301. def OAI.SplitTangent.ActualCauchy.IsActualSolution line 3590
  302. theorem OAI.SplitTangent.ActualCauchy.existsUnique_actualSolution line 3598
  303. theorem OAI.SplitTangent.ActualCauchy.IsActualSolution.pointwise line 3604
  304. def OAI.SplitTangent.HolomorphicJets.CauchyOn line 3623
  305. theorem OAI.SplitTangent.HolomorphicJets.cauchyOn_recurrence line 3630
  306. theorem OAI.SplitTangent.HolomorphicJets.exists_cauchyOn line 3647
  307. theorem OAI.SplitTangent.HolomorphicJets.cauchyOn_unique line 3668
  308. theorem OAI.SplitTangent.HolomorphicJets.CauchyOn.mono line 3699
  309. theorem OAI.SplitTangent.HolomorphicJets.CauchyOn.target line 3712
  310. theorem OAI.SplitTangent.HolomorphicJets.cauchyOn_target_glue line 3741
  311. def OAI.SplitTangent.HolomorphicJets.familySeries line 3758
  312. theorem OAI.SplitTangent.HolomorphicJets.familySeries_eval line 3764
  313. theorem OAI.SplitTangent.HolomorphicJets.familySeries_coeff line 3771
  314. theorem OAI.SplitTangent.HolomorphicJets.sourceNormal_inv line 3775
  315. theorem OAI.SplitTangent.HolomorphicJets.normalVector_of_series line 3808
  316. theorem OAI.SplitTangent.HolomorphicJets.tangentVector_of_series line 3819
  317. def OAI.SplitTangent.HolomorphicJets.sourceFamily line 3826
  318. theorem OAI.SplitTangent.HolomorphicJets.sourceFamily_eval line 3833
  319. theorem OAI.SplitTangent.HolomorphicJets.CauchyOn.source line 3849
  320. theorem OAI.SplitTangent.HolomorphicJets.cauchyOn_source_glue line 3883
  321. theorem OAI.SplitTangent.HolomorphicJets.CauchyOn.congr_initial line 3899
  322. theorem OAI.SplitTangent.TangentSplitting.coordinateMatrix_intertwining line 3912
  323. def OAI.SplitTangent.TangentSplitting.coordinateDomain line 3935
  324. def OAI.SplitTangent.TangentSplitting.coordinateCurve line 3938
  325. theorem OAI.SplitTangent.TangentSplitting.coordinateDomain_open line 3941
  326. theorem OAI.SplitTangent.TangentSplitting.coordinateCurve_analytic_formal line 3945
  327. def OAI.SplitTangent.TangentSplitting.localJet line 3955
  328. theorem OAI.SplitTangent.TangentSplitting.localJet_solution line 3963
  329. theorem OAI.SplitTangent.TangentSplitting.localJet_target_glue line 3970
  330. def OAI.SplitTangent.TangentSplitting.scalarCoordinate line 4019
  331. theorem OAI.SplitTangent.TangentSplitting.scalarCoordinate_analytic line 4022
  332. theorem OAI.SplitTangent.TangentSplitting.localJet_scalar_glue line 4037
  333. def OAI.SplitTangent.TangentSplitting.scalarJet line 4078
  334. theorem OAI.SplitTangent.TangentSplitting.scalarJet_eq_local line 4083
  335. theorem OAI.SplitTangent.TangentSplitting.scalarJet_constant line 4091
  336. theorem OAI.SplitTangent.TangentSplitting.scalarJet_analytic line 4104
  337. theorem OAI.SplitTangent.TangentSplitting.localJet_source_glue line 4128
  338. theorem OAI.SplitTangent.TangentSplitting.scalarJet_source_glue line 4162
  339. theorem OAI.SplitTangent.TangentSplitting.scalarJet_congr line 4199
  340. theorem OAI.SplitTangent.TangentSplitting.scalarJet_mul line 4214
  341. theorem OAI.SplitTangent.TangentSplitting.scalarJet_const line 4227
  342. def OAI.SplitTangent.ProjectiveLine.MeromorphicAtInfinity line 4242
  343. theorem OAI.SplitTangent.ProjectiveLine.finite_nonanalytic line 4247
  344. theorem OAI.SplitTangent.ProjectiveLine.exists_polynomial_denominator line 4273
  345. theorem OAI.SplitTangent.ProjectiveLine.polynomial_growth_atInfinity line 4299
  346. theorem OAI.SplitTangent.ProjectiveLine.iteratedDeriv_zero_of_tail_growth line 4322
  347. theorem OAI.SplitTangent.ProjectiveLine.exists_polynomial_of_entire line 4343
  348. theorem OAI.SplitTangent.ProjectiveLine.meromorphicAt_polynomial_eval line 4356
  349. theorem OAI.SplitTangent.ProjectiveLine.rationality line 4364
  350. theorem OAI.SplitTangent.projectiveCoordinates_change line 4382
  351. theorem OAI.SplitTangent.projective_ratio_meromorphic line 4393
  352. theorem OAI.SplitTangent.rationalCurve_ratio_meromorphicAtInfinity line 4416
  353. theorem OAI.SplitTangent.rationalCurve_ratios_are_rational line 4426
  354. theorem OAI.SplitTangent.PolynomialTuple.gcd_mem_span line 4438
  355. theorem OAI.SplitTangent.PolynomialTuple.bezout line 4452
  356. theorem OAI.SplitTangent.PolynomialTuple.basepoint_free line 4459
  357. theorem OAI.SplitTangent.PolynomialTuple.frequently_eval_ne_zero line 4468
  358. theorem OAI.SplitTangent.PolynomialTuple.common_denominator line 4476
  359. theorem OAI.SplitTangent.rationalCurve_polynomial_presentation line 4494
  360. theorem OAI.SplitTangent.PolynomialTuple.primitive_of_basepoint_free line 4552
  361. theorem OAI.SplitTangent.PolynomialTuple.reflect_transition line 4563
  362. theorem OAI.SplitTangent.PolynomialTuple.exists_primitive_reflection line 4571
  363. theorem OAI.SplitTangent.rationalCurve_two_chart_polynomials line 4604
  364. theorem OAI.SplitTangent.ProjectiveEmbedding.scalar_holomorphic line 4653
  365. theorem OAI.SplitTangent.projectiveCoordinates_mul line 4659
  366. theorem OAI.SplitTangent.polynomial_presentation_patch line 4669
  367. def OAI.SplitTangent.TangentSplitting.projectiveChartData line 4694
  368. theorem OAI.SplitTangent.TangentSplitting.exists_projective_formal_data line 4729
  369. theorem OAI.SplitTangent.TangentSplitting.exists_convergent_projective_patch line 4769
  370. theorem OAI.AnalyticRetraction.localInverse_analytic line 4797
  371. theorem OAI.AnalyticRetraction.exists_left_inverse line 4812
  372. theorem OAI.SplitTangent.HolomorphicJets.composeJet_analyticJet line 4845
  373. theorem OAI.SplitTangent.HolomorphicJets.composeJet_id line 4852
  374. theorem OAI.SplitTangent.HolomorphicJets.composeJet_germ line 4859
  375. theorem OAI.SplitTangent.HolomorphicJets.composeJet_assoc line 4865
  376. theorem OAI.SplitTangent.HolomorphicJets.analyticJet_eq_germ line 4872
  377. theorem OAI.SplitTangent.HolomorphicJets.lift_convergent line 4883
  378. theorem OAI.SplitTangent.HolomorphicJets.lift_convergent_family line 4908
  379. def OAI.SplitTangent.ProjectiveEmbedding.withinChart line 4945
  380. theorem OAI.SplitTangent.ProjectiveEmbedding.withinChart_analytic line 4948
  381. theorem OAI.SplitTangent.ProjectiveEmbedding.withinChart_immersion line 4956
  382. theorem OAI.SplitTangent.TangentSplitting.exists_convergent_manifold_jet line 4997
  383. theorem OAI.SplitTangent.TangentSplitting.exists_holomorphic_cauchy_germ line 5040
  384. theorem OAI.SplitTangent.HolomorphicJets.taylorSeries_eq_germ line 5069
  385. theorem OAI.SplitTangent.HolomorphicJets.joint_germ_of_slice_germs line 5079
  386. theorem OAI.SplitTangent.HolomorphicJets.normalVector_analyticJet line 5103
  387. theorem OAI.SplitTangent.HolomorphicJets.tangentVector_analyticJet line 5117
  388. theorem OAI.SplitTangent.HolomorphicJets.substitutedMatrix_analyticJet line 5128
  389. theorem OAI.SplitTangent.HolomorphicJets.cauchy_analytic_fiber line 5141
  390. theorem OAI.SplitTangent.HolomorphicJets.cauchy_analytic_joint line 5175
  391. theorem OAI.SplitTangent.TangentSplitting.exists_cauchy_coordinates line 5211
  392. theorem OAI.SplitTangent.TangentSplitting.cauchy_chart_inverse line 5243
  393. theorem OAI.SplitTangent.TangentSplitting.exists_actual_cauchy_germ line 5284
  394. theorem OAI.SplitTangent.HolomorphicJets.image_eq_of_jets line 5313
  395. def OAI.SplitTangent.DiagonalRationality.normalBiPolynomial line 5349
  396. theorem OAI.SplitTangent.DiagonalRationality.polynomialFunction_X line 5352
  397. theorem OAI.SplitTangent.DiagonalRationality.normalBiPolynomial_map line 5356
  398. theorem OAI.SplitTangent.DiagonalRationality.exists_bivariate_of_coefficients line 5365
  399. theorem OAI.SplitTangent.DiagonalRationality.bivariate_of_normal_division line 5377
  400. def OAI.SplitTangent.DiagonalRationality.bivariateEvaluation line 5389
  401. theorem OAI.SplitTangent.DiagonalRationality.evaluate_polynomial_map line 5392
  402. theorem OAI.SplitTangent.FormalProjective.reconstruct_projective_bivariate line 5405
  403. theorem OAI.SplitTangent.TangentSplitting.exists_bivariate_cauchy_patch line 5451
  404. theorem OAI.SplitTangent.TangentSplitting.exists_rational_cauchy_coordinates line 5475
  405. abbrev OAI.SplitTangent.RationalSurface.K line 5528
  406. abbrev OAI.SplitTangent.RationalSurface.R line 5531
  407. abbrev OAI.SplitTangent.RationalSurface.B line 5532
  408. def OAI.SplitTangent.RationalSurface.eval line 5534
  409. theorem OAI.SplitTangent.RationalSurface.finite_common_zeros line 5540
  410. theorem OAI.SplitTangent.RationalSurface.common_denominator line 5563
  411. theorem OAI.SplitTangent.RationalSurface.no_vertical_component line 5583
  412. theorem OAI.SplitTangent.RationalSurface.generic_gcd_eq_one line 5600
  413. theorem OAI.SplitTangent.RationalSurface.generic_gcd_mem_span line 5633
  414. theorem OAI.SplitTangent.RationalSurface.vertical_bezout line 5648
  415. theorem OAI.SplitTangent.RationalSurface.finite_zero_set line 5662
  416. theorem OAI.SplitTangent.RationalSurface.eval_analytic line 5668
  417. theorem OAI.SplitTangent.RationalSurface.polynomial_ratio_tuple line 5680
  418. theorem OAI.SplitTangent.RationalSurface.primitive_ratio_tuple line 5696
  419. theorem OAI.SplitTangent.TangentSplitting.exists_rational_tangent_germ line 5738
  420. def OAI.SplitTangent.ProjectiveEmbedding.Incidence line 5816
  421. theorem OAI.SplitTangent.ProjectiveEmbedding.incidence_iff_coordinates line 5821
  422. theorem OAI.SplitTangent.ProjectiveEmbedding.incidence_iff_projective line 5835
  423. theorem OAI.SplitTangent.ProjectiveEmbedding.incidence_unique line 5870
  424. theorem OAI.SplitTangent.ProjectiveEmbedding.isClosed_incidence line 5875
  425. theorem OAI.SplitTangent.ProjectiveEmbedding.isClosed_cone line 5906
  426. theorem OAI.SplitTangent.ProjectiveEmbedding.incidence_localizes line 5916
  427. def OAI.SplitTangent.ProjectiveEmbedding.normalize line 5932
  428. theorem OAI.SplitTangent.ProjectiveEmbedding.normalize_analytic line 5935
  429. theorem OAI.SplitTangent.ProjectiveEmbedding.incidence_iff_normalize line 5942
  430. theorem OAI.SplitTangent.ProjectiveEmbedding.cone_local_equations line 5958
  431. theorem OAI.SplitTangent.ProjectiveEmbedding.cone_local_equations_any line 6017
  432. theorem OAI.SplitTangent.ProjectiveEmbedding.cone_continuation line 6037
  433. theorem OAI.SplitTangent.ProjectiveEmbedding.exists_local_lift line 6049
  434. theorem OAI.SplitTangent.ProjectiveEmbedding.holomorphic_of_incidence line 6098
  435. theorem OAI.SplitTangent.ProjectiveEmbedding.exists_global_regular_lift line 6109
  436. theorem OAI.SplitTangent.TangentSplitting.chart_derivative line 6154
  437. theorem OAI.SplitTangent.TangentSplitting.chart_pde_iff line 6169
  438. theorem OAI.SplitTangent.TangentSplitting.pde_local_equations line 6195
  439. theorem OAI.SplitTangent.TangentSplitting.pde_continuation line 6228
  440. theorem OAI.SplitTangent.TangentSplitting.exists_global_regular_tangent_box line 6245
  441. def OAI.SplitTangent.TangentSplitting.WedgeAt line 6309
  442. def OAI.SplitTangent.TangentSplitting.projectedInChart line 6313
  443. lemma OAI.SplitTangent.TangentSplitting.projectedInChart_eq line 6317
  444. lemma OAI.SplitTangent.TangentSplitting.projectedInChart_analytic line 6331
  445. lemma OAI.SplitTangent.TangentSplitting.chart_wedge_iff line 6352
  446. theorem OAI.SplitTangent.TangentSplitting.WedgeAt.comp line 6370
  447. theorem OAI.SplitTangent.TangentSplitting.wedgeAt_of_frequently line 6382
  448. theorem OAI.SplitTangent.ExceptionalTangency.factor_fderiv line 6409
  449. theorem OAI.SplitTangent.ExceptionalTangency.kills_tangent_of_wedge line 6425
  450. theorem OAI.SplitTangent.ExceptionalTangency.complementary_kills_tangent line 6460
  451. theorem OAI.SplitTangent.ComplexManifold.chart_derivative line 6485
  452. theorem OAI.SplitTangent.ComplexManifold.locally_eq_of_mfderiv_zero line 6501
  453. theorem OAI.SplitTangent.ComplexManifold.eq_of_mfderiv_zero line 6526
  454. theorem OAI.SplitTangent.ComplexManifold.curve_eq_of_mfderiv_zero_off_finite line 6540
  455. lemma OAI.SplitTangent.ExceptionalTangency.kills_second_of_wedge line 6559
  456. theorem OAI.SplitTangent.TangentSplitting.kills_exceptional_of_wedge line 6595
  457. theorem OAI.SplitTangent.TangentSplitting.constant_exceptional line 6620
  458. abbrev OAI.SplitTangent.FormalBlowup.D line 6664
  459. abbrev OAI.SplitTangent.FormalBlowup.x line 6665
  460. abbrev OAI.SplitTangent.FormalBlowup.y line 6666
  461. lemma OAI.SplitTangent.FormalBlowup.x_ne_zero line 6668
  462. def OAI.SplitTangent.FormalBlowup.highOrder line 6674
  463. lemma OAI.SplitTangent.FormalBlowup.mem_highOrder line 6685
  464. lemma OAI.SplitTangent.FormalBlowup.highOrder_one line 6700
  465. def OAI.SplitTangent.FormalBlowup.coordinateSubstitution line 6707
  466. lemma OAI.SplitTangent.FormalBlowup.coordinateSubstitution_hasSubst line 6709
  467. def OAI.SplitTangent.FormalBlowup.blowup line 6714
  468. lemma OAI.SplitTangent.FormalBlowup.substituted_monomial line 6716
  469. lemma OAI.SplitTangent.FormalBlowup.exceptional_pow_dvd line 6723
  470. def OAI.SplitTangent.FormalBlowup.transform line 6738
  471. lemma OAI.SplitTangent.FormalBlowup.exceptional_mul_transform line 6752
  472. lemma OAI.SplitTangent.FormalBlowup.transform_mul line 6755
  473. def OAI.SplitTangent.FormalBlowup.exp line 6762
  474. lemma OAI.SplitTangent.FormalBlowup.exp_zero line 6764
  475. lemma OAI.SplitTangent.FormalBlowup.exp_one line 6765
  476. lemma OAI.SplitTangent.FormalBlowup.exp_eta line 6767
  477. lemma OAI.SplitTangent.FormalBlowup.variable_monomial line 6770
  478. lemma OAI.SplitTangent.FormalBlowup.coeff_blowup line 6774
  479. lemma OAI.SplitTangent.FormalBlowup.coeff_x_pow_mul line 6790
  480. lemma OAI.SplitTangent.FormalBlowup.coeff_transform_initial line 6802
  481. lemma OAI.SplitTangent.FormalBlowup.monomial_mem_highOrder line 6813
  482. lemma OAI.SplitTangent.FormalBlowup.blowup_x line 6819
  483. lemma OAI.SplitTangent.FormalBlowup.blowup_y line 6824
  484. lemma OAI.SplitTangent.FormalBlowup.transform_monomial line 6829
  485. def OAI.SplitTangent.FormalBlowup.yEmbedding line 6837
  486. def OAI.SplitTangent.FormalBlowup.row line 6838
  487. def OAI.SplitTangent.FormalBlowup.insertRow line 6839
  488. lemma OAI.SplitTangent.FormalBlowup.row_coeff line 6841
  489. lemma OAI.SplitTangent.FormalBlowup.insertRow_coeff line 6846
  490. lemma OAI.SplitTangent.FormalBlowup.insertRow_X line 6851
  491. lemma OAI.SplitTangent.FormalBlowup.self_sub_insertRow line 6854
  492. lemma OAI.SplitTangent.FormalBlowup.row_initial_order_le line 6862
  493. lemma OAI.SplitTangent.FormalBlowup.initial_factor line 6875
  494. lemma OAI.SplitTangent.FormalBlowup.submodule_eq_top_of_nilpotent line 6888
  495. lemma OAI.SplitTangent.FormalBlowup.exceptional_power_in_sup line 6917
  496. lemma OAI.SplitTangent.FormalBlowup.low_remainder line 6932
  497. def OAI.SplitTangent.FormalBlowup.transformIdeal line 6946
  498. lemma OAI.SplitTangent.FormalBlowup.transform_mem line 6949
  499. lemma OAI.SplitTangent.FormalBlowup.exists_x_pow_mem line 6954
  500. lemma OAI.SplitTangent.FormalBlowup.exists_x_pow_mem_transform line 6961
  501. lemma OAI.SplitTangent.FormalBlowup.insertRow_trunc line 6975
  502. lemma OAI.SplitTangent.FormalBlowup.quotient_transform_surjective line 6989
  503. lemma OAI.SplitTangent.FormalBlowup.strict_transform_surjective line 7035
  504. theorem OAI.SplitTangent.FormalBlowup.finite_colength_strict_drop line 7049
  505. lemma OAI.SplitTangent.FormalBlowup.transform_of_span_mem line 7090
  506. lemma OAI.SplitTangent.FormalBlowup.transformIdeal_span line 7107
  507. lemma OAI.SplitTangent.FormalBlowup.exists_minimal_order line 7124
  508. lemma OAI.SplitTangent.FormalBlowup.coeff_blowup_eq_zero line 7155
  509. lemma OAI.SplitTangent.FormalBlowup.row_transform_coeff_eq_zero line 7167
  510. def OAI.SplitTangent.FormalBlowup.initialPolynomial line 7177
  511. lemma OAI.SplitTangent.FormalBlowup.initialPolynomial_coe line 7180
  512. lemma OAI.SplitTangent.FormalBlowup.initialPolynomial_natDegree_le line 7188
  513. lemma OAI.SplitTangent.FormalBlowup.initialPolynomial_ne_zero line 7192
  514. lemma OAI.SplitTangent.FormalBlowup.finite_exceptional_base_set line 7203
  515. abbrev OAI.SplitTangent.FormalBlowup.B line 7213
  516. def OAI.SplitTangent.FormalBlowup.polynomialTransform line 7215
  517. lemma OAI.SplitTangent.FormalBlowup.blowup_monomial line 7218
  518. lemma OAI.SplitTangent.FormalBlowup.polynomialTransform_factor line 7223
  519. lemma OAI.SplitTangent.FormalBlowup.transform_polynomial line 7243
  520. lemma OAI.SplitTangent.FormalBlowup.mem_ideal_of_rectangle_zero line 7250
  521. def OAI.SplitTangent.FormalBlowup.rectangleMap line 7275
  522. lemma OAI.SplitTangent.FormalBlowup.rectangleMap_apply line 7278
  523. lemma OAI.SplitTangent.FormalBlowup.rectangleMap_coeff line 7282
  524. theorem OAI.SplitTangent.FormalBlowup.finite_colength_of_coordinate_powers line 7302
  525. def OAI.SplitTangent.FormalBlowup.shearCoordinates line 7319
  526. lemma OAI.SplitTangent.FormalBlowup.shearCoordinates_hasSubst line 7321
  527. def OAI.SplitTangent.FormalBlowup.shear line 7326
  528. lemma OAI.SplitTangent.FormalBlowup.shear_x line 7328
  529. lemma OAI.SplitTangent.FormalBlowup.shear_y line 7331
  530. lemma OAI.SplitTangent.FormalBlowup.shear_C line 7334
  531. lemma OAI.SplitTangent.FormalBlowup.shear_neg_shear line 7337
  532. def OAI.SplitTangent.FormalBlowup.shearEquiv line 7355
  533. lemma OAI.SplitTangent.FormalBlowup.order_le_shear line 7361
  534. lemma OAI.SplitTangent.FormalBlowup.order_shear line 7372
  535. lemma OAI.SplitTangent.FormalBlowup.shear_mem_highOrder_iff line 7378
  536. def OAI.SplitTangent.FormalBlowup.shearIdeal line 7383
  537. def OAI.SplitTangent.FormalBlowup.shearQuotientEquiv line 7385
  538. lemma OAI.SplitTangent.FormalBlowup.shearIdeal_ne_top line 7389
  539. theorem OAI.SplitTangent.FormalBlowup.colength_drop_at_direction line 7394
  540. abbrev OAI.SplitTangent.PolynomialBlowup.P line 7413
  541. def OAI.SplitTangent.PolynomialBlowup.embed line 7415
  542. lemma OAI.SplitTangent.PolynomialBlowup.embed_apply line 7421
  543. lemma OAI.SplitTangent.PolynomialBlowup.embed_X line 7422
  544. lemma OAI.SplitTangent.PolynomialBlowup.embed_C line 7423
  545. def OAI.SplitTangent.PolynomialBlowup.shift line 7427
  546. def OAI.SplitTangent.PolynomialBlowup.shear line 7431
  547. def OAI.SplitTangent.PolynomialBlowup.blowup line 7434
  548. lemma OAI.SplitTangent.PolynomialBlowup.shift_X₀ line 7437
  549. lemma OAI.SplitTangent.PolynomialBlowup.shift_X₁ line 7438
  550. lemma OAI.SplitTangent.PolynomialBlowup.shear_X₀ line 7439
  551. lemma OAI.SplitTangent.PolynomialBlowup.shear_X₁ line 7440
  552. lemma OAI.SplitTangent.PolynomialBlowup.blowup_X₀ line 7441
  553. lemma OAI.SplitTangent.PolynomialBlowup.blowup_X₁ line 7442
  554. lemma OAI.SplitTangent.PolynomialBlowup.shift_C line 7443
  555. lemma OAI.SplitTangent.PolynomialBlowup.shear_C line 7444
  556. lemma OAI.SplitTangent.PolynomialBlowup.blowup_C line 7445
  557. lemma OAI.SplitTangent.PolynomialBlowup.embed_shear line 7447
  558. lemma OAI.SplitTangent.PolynomialBlowup.embed_blowup line 7454
  559. lemma OAI.SplitTangent.PolynomialBlowup.polynomial_factor line 7463
  560. lemma OAI.SplitTangent.PolynomialBlowup.shift_blowup line 7470
  561. lemma OAI.SplitTangent.PolynomialBlowup.transform_at_direction line 7481
  562. def OAI.SplitTangent.PolynomialBlowup.baseIdeal line 7492
  563. def OAI.SplitTangent.PolynomialBlowup.transformPreimage line 7495
  564. lemma OAI.SplitTangent.PolynomialBlowup.transform_span line 7514
  565. lemma OAI.SplitTangent.PolynomialBlowup.shear_baseIdeal line 7532
  566. lemma OAI.SplitTangent.PolynomialBlowup.baseIdeal_shift_transform line 7540
  567. lemma OAI.SplitTangent.FormalBlowup.shearIdeal_le_highOrder line 7557
  568. lemma OAI.SplitTangent.FormalBlowup.order_eq_of_initial line 7563
  569. lemma OAI.SplitTangent.FormalBlowup.initial_of_order_eq line 7570
  570. theorem OAI.SplitTangent.FormalBlowup.uniform_colength_drop line 7578
  571. def OAI.SplitTangent.FormalBlowup.swapCoordinates line 7596
  572. lemma OAI.SplitTangent.FormalBlowup.swapCoordinates_hasSubst line 7597
  573. def OAI.SplitTangent.FormalBlowup.swap line 7601
  574. lemma OAI.SplitTangent.FormalBlowup.swap_x line 7602
  575. lemma OAI.SplitTangent.FormalBlowup.swap_y line 7606
  576. lemma OAI.SplitTangent.FormalBlowup.swap_C line 7610
  577. lemma OAI.SplitTangent.FormalBlowup.swap_swap line 7612
  578. def OAI.SplitTangent.FormalBlowup.swapEquiv line 7625
  579. lemma OAI.SplitTangent.FormalBlowup.order_le_swap line 7628
  580. lemma OAI.SplitTangent.FormalBlowup.order_swap line 7638
  581. lemma OAI.SplitTangent.FormalBlowup.swap_mem_highOrder_iff line 7643
  582. def OAI.SplitTangent.FormalBlowup.swapIdeal line 7646
  583. def OAI.SplitTangent.FormalBlowup.swapQuotientEquiv line 7647
  584. lemma OAI.SplitTangent.FormalBlowup.swapIdeal_le_highOrder line 7649
  585. def OAI.SplitTangent.PolynomialBlowup.swap line 7661
  586. lemma OAI.SplitTangent.PolynomialBlowup.swap_X₀ line 7662
  587. lemma OAI.SplitTangent.PolynomialBlowup.swap_X₁ line 7663
  588. lemma OAI.SplitTangent.PolynomialBlowup.embed_swap line 7664
  589. lemma OAI.SplitTangent.PolynomialBlowup.swap_baseIdeal line 7670
  590. def OAI.SplitTangent.PolynomialBlowup.child line 7680
  591. lemma OAI.SplitTangent.PolynomialBlowup.child_finite_drop line 7683
  592. lemma OAI.SplitTangent.PolynomialBlowup.swap_finite line 7694
  593. lemma OAI.SplitTangent.PolynomialBlowup.swap_finrank line 7699
  594. lemma OAI.SplitTangent.PolynomialBlowup.swap_child_finite_drop line 7704
  595. def OAI.SplitTangent.PolynomialBlowup.ResolvesWithin line 7727
  596. lemma OAI.SplitTangent.PolynomialBlowup.resolvesWithin_mono line 7733
  597. theorem OAI.SplitTangent.PolynomialBlowup.resolvesWithin_colength line 7748
  598. def OAI.SplitTangent.PolynomialBlowup.valueHom line 7776
  599. def OAI.SplitTangent.PolynomialBlowup.value line 7777
  600. lemma OAI.SplitTangent.PolynomialBlowup.value_X₀ line 7778
  601. lemma OAI.SplitTangent.PolynomialBlowup.value_X₁ line 7779
  602. lemma OAI.SplitTangent.PolynomialBlowup.value_C line 7780
  603. lemma OAI.SplitTangent.PolynomialBlowup.value_add line 7781
  604. lemma OAI.SplitTangent.PolynomialBlowup.value_mul line 7782
  605. lemma OAI.SplitTangent.PolynomialBlowup.value_pow line 7783
  606. def OAI.SplitTangent.PolynomialBlowup.constant line 7785
  607. lemma OAI.SplitTangent.PolynomialBlowup.constant_embed line 7788
  608. lemma OAI.SplitTangent.PolynomialBlowup.baseIdeal_ne_top_iff line 7797
  609. lemma OAI.SplitTangent.PolynomialBlowup.baseIdeal_eq_top_iff line 7813
  610. lemma OAI.SplitTangent.PolynomialBlowup.value_shift line 7818
  611. lemma OAI.SplitTangent.PolynomialBlowup.value_blowup line 7824
  612. lemma OAI.SplitTangent.PolynomialBlowup.value_swap line 7830
  613. lemma OAI.SplitTangent.PolynomialBlowup.child_factor line 7839
  614. def OAI.SplitTangent.PolynomialBlowup.linePolynomial line 7849
  615. lemma OAI.SplitTangent.PolynomialBlowup.linePolynomial_eval line 7850
  616. lemma OAI.SplitTangent.PolynomialBlowup.row_embed line 7857
  617. lemma OAI.SplitTangent.PolynomialBlowup.exists_generator_initial line 7875
  618. theorem OAI.SplitTangent.PolynomialBlowup.finite_bad_directions line 7894
  619. lemma OAI.SplitTangent.PolynomialBlowup.value_analytic line 7921
  620. def OAI.SplitTangent.PolynomialBlowup.IsolatedAtOrigin line 7933
  621. lemma OAI.SplitTangent.PolynomialBlowup.finite_isolated line 7936
  622. lemma OAI.SplitTangent.PolynomialBlowup.child_isolated line 7943
  623. lemma OAI.SplitTangent.PolynomialBlowup.X_dvd_of_linePolynomial_eq_zero line 7978
  624. lemma OAI.SplitTangent.PolynomialBlowup.linePolynomial_eq_zero_of_X_dvd line 7994
  625. lemma OAI.SplitTangent.PolynomialBlowup.blowup_injective line 7999
  626. theorem OAI.SplitTangent.PolynomialBlowup.coordinate_exceptional_factor line 8011
  627. lemma OAI.SplitTangent.PolynomialBlowup.power_times_unit_product line 8031
  628. lemma OAI.SplitTangent.PolynomialBlowup.coordinate_power_of_finite_zeros line 8049
  629. theorem OAI.SplitTangent.PolynomialBlowup.finite_colength_of_finite_zeros line 8086
  630. lemma OAI.SplitTangent.PolynomialBlowup.finite_zeros_shift line 8093
  631. theorem OAI.SplitTangent.IsolatedZero.lower_bound_on_disc line 8106
  632. theorem OAI.SplitTangent.IsolatedZero.nonzero_of_punctured_nonzero line 8126
  633. theorem OAI.SplitTangent.IsolatedZero.nonzero_of_punctured_nonzero_at line 8183
  634. theorem OAI.SplitTangent.ProjectiveEmbedding.nonzero_of_continuous_incidence line 8206
  635. theorem OAI.SplitTangent.ProjectiveEmbedding.holomorphic_of_continuous_punctured_incidence line 8226
  636. def OAI.SplitTangent.AffineBlowup.first line 8250
  637. def OAI.SplitTangent.AffineBlowup.second line 8251
  638. theorem OAI.SplitTangent.AffineBlowup.tendsto_of_constant_exceptional line 8257
  639. lemma OAI.SplitTangent.ProjectiveEmbedding.incidence_zero line 8317
  640. lemma OAI.SplitTangent.ProjectiveEmbedding.incidence_smul_iff line 8321
  641. def OAI.SplitTangent.ProjectiveEmbedding.coneLift line 8339
  642. lemma OAI.SplitTangent.ProjectiveEmbedding.coneLift_incidence line 8343
  643. lemma OAI.SplitTangent.ProjectiveEmbedding.coneLift_eq line 8348
  644. lemma OAI.SplitTangent.ProjectiveEmbedding.coneLift_smul line 8352
  645. lemma OAI.SplitTangent.TangentSplitting.WedgeAt.congr line 8365
  646. lemma OAI.SplitTangent.PolynomialBlowup.value_sub line 8376
  647. lemma OAI.SplitTangent.PolynomialBlowup.shift_shift line 8379
  648. lemma OAI.SplitTangent.PolynomialBlowup.shift_zero line 8385
  649. lemma OAI.SplitTangent.PolynomialBlowup.shift_injective line 8391
  650. lemma OAI.SplitTangent.PolynomialBlowup.polynomial_swap_swap line 8395
  651. lemma OAI.SplitTangent.PolynomialBlowup.polynomial_swap_injective line 8401
  652. lemma OAI.SplitTangent.AffineBlowup.tendsto_of_local_constant_exceptional line 8410
  653. def OAI.SplitTangent.BasePointRemoval.tuple line 8448
  654. def OAI.SplitTangent.BasePointRemoval.lift line 8450
  655. lemma OAI.SplitTangent.BasePointRemoval.tuple_analytic line 8453
  656. lemma OAI.SplitTangent.BasePointRemoval.tuple_child line 8456
  657. lemma OAI.SplitTangent.BasePointRemoval.lift_holomorphic line 8461
  658. lemma OAI.SplitTangent.BasePointRemoval.frequently_first_ne line 8468
  659. lemma OAI.SplitTangent.BasePointRemoval.blowup_contDiff line 8477
  660. lemma OAI.SplitTangent.BasePointRemoval.cone_child line 8480
  661. def OAI.SplitTangent.BasePointRemoval.Admissible line 8499
  662. lemma OAI.SplitTangent.BasePointRemoval.value_child_coordinate line 8504
  663. lemma OAI.SplitTangent.BasePointRemoval.lift_child_eq line 8510
  664. lemma OAI.SplitTangent.BasePointRemoval.admissible_child line 8517
  665. lemma OAI.SplitTangent.BasePointRemoval.tuple_swap line 8562
  666. lemma OAI.SplitTangent.BasePointRemoval.admissible_swap line 8566
  667. lemma OAI.SplitTangent.BasePointRemoval.isolated_swap line 8588
  668. lemma OAI.SplitTangent.BasePointRemoval.tuple_shift line 8596
  669. lemma OAI.SplitTangent.BasePointRemoval.regular_shift_data line 8600
  670. lemma OAI.SplitTangent.BasePointRemoval.transformed_curve_data line 8632
  671. lemma OAI.SplitTangent.BasePointRemoval.transformed_curve_constant line 8644
  672. lemma OAI.SplitTangent.BasePointRemoval.tuple_transformed_factor line 8668
  673. lemma OAI.SplitTangent.BasePointRemoval.transformed_lift_near line 8675
  674. lemma OAI.SplitTangent.BasePointRemoval.lift_swap line 8693
  675. theorem OAI.SplitTangent.BasePointRemoval.nonzero_of_regular_children line 8699
  676. lemma OAI.SplitTangent.BasePointRemoval.child_coordinate_nonzero line 8756
  677. lemma OAI.SplitTangent.BasePointRemoval.child_coordinate_origin line 8764
  678. lemma OAI.SplitTangent.BasePointRemoval.swap_child_isolated line 8768
  679. theorem OAI.SplitTangent.BasePointRemoval.no_basepoint line 8786
  680. theorem OAI.SplitTangent.BasePointRemoval.nonzero_everywhere line 8826
  681. lemma OAI.SplitTangent.TangentSplitting.wedges_of_pde line 8878
  682. lemma OAI.SplitTangent.ComplexManifold.equality_local_equations line 8923
  683. theorem OAI.SplitTangent.ComplexManifold.eqOn_of_eventuallyEq line 8952
  684. def OAI.SplitTangent.RationalSurface.toMv line 8966
  685. lemma OAI.SplitTangent.RationalSurface.value_toMv line 8969
  686. theorem OAI.SplitTangent.TangentSplitting.exists_affine_polynomial_tangent_box line 8989
  687. theorem OAI.SplitTangent.TangentSplitting.exists_affine_tangent_box line 9049
  688. theorem OAI.SplitTangent.TangentSplitting.exists_affine_box line 9066
  689. def OAI.SplitTangent.RationalSurface.RationalOn line 9123
  690. lemma OAI.SplitTangent.RationalSurface.RationalOn.const line 9126
  691. lemma OAI.SplitTangent.RationalSurface.RationalOn.fst line 9130
  692. lemma OAI.SplitTangent.RationalSurface.RationalOn.snd line 9134
  693. lemma OAI.SplitTangent.RationalSurface.RationalOn.add line 9138
  694. lemma OAI.SplitTangent.RationalSurface.RationalOn.neg line 9151
  695. lemma OAI.SplitTangent.RationalSurface.RationalOn.sub line 9158
  696. lemma OAI.SplitTangent.RationalSurface.RationalOn.mul line 9162
  697. lemma OAI.SplitTangent.RationalSurface.RationalOn.inv line 9175
  698. lemma OAI.SplitTangent.RationalSurface.rational_polynomial_eval₂ line 9183
  699. lemma OAI.SplitTangent.RationalSurface.RationalOn.eval_comp line 9193
  700. theorem OAI.SplitTangent.RationalSurface.primitive_tuple_of_rational line 9202
  701. lemma OAI.SplitTangent.TangentSplitting.wedges_iff_tangency line 9249
  702. theorem OAI.SplitTangent.TangentSplitting.extend_rational_tangent_map line 9297
  703. lemma OAI.SplitTangent.TangentSplitting.tangency_comp_changeChart line 9361
  704. lemma OAI.SplitTangent.TangentSplitting.rational_changeChart_fst line 9387
  705. lemma OAI.SplitTangent.TangentSplitting.rational_changeChart_snd line 9393
  706. theorem OAI.SplitTangent.TangentSplitting.exists_projective_tangent_box line 9401