OAI/Geometry/SplitTangent/TensorVanishing.lean

GitHub source file

244 declarations, 0 contain sorry, 0 declared as axioms

Tensor Vanishing.

  1. def OAI.HolomorphicFrobenius.InvolutiveAt line 25
  2. lemma OAI.SplitTangent.ProductTransition.eventually_factors_snd line 40
  3. lemma OAI.SplitTangent.ProductTransition.eventually_factors_fst line 68
  4. theorem OAI.SplitTangent.ProductTransition.eventually_product line 91
  5. structure OAI.SplitTangent.AlignedProductChart line 123
  6. lemma OAI.SplitTangent.AlignedProductChart.mdifferentiable line 143
  7. lemma OAI.SplitTangent.AlignedProductChart.holomorphicAt line 147
  8. lemma OAI.SplitTangent.AlignedProductChart.inverse_holomorphicAt line 151
  9. lemma OAI.SplitTangent.AlignedProductChart.inverse_first line 155
  10. lemma OAI.SplitTangent.AlignedProductChart.inverse_second line 174
  11. theorem OAI.SplitTangent.AlignedProductChart.transition_axes line 195
  12. theorem OAI.SplitTangent.AlignedProductChart.transition_product line 226
  13. abbrev OAI.SplitTangent.chartDerivative line 248
  14. lemma OAI.SplitTangent.chartDerivative_isInvertible line 251
  15. lemma OAI.SplitTangent.chartDerivative_inverse line 262
  16. lemma OAI.SplitTangent.chartPullback_holomorphicAt line 280
  17. lemma OAI.SplitTangent.chartPullback_bracket line 293
  18. lemma OAI.SplitTangent.TangentSplitting.coordinateProjector_range_iff line 323
  19. theorem OAI.SplitTangent.TangentSplitting.coordinateProjector_involutive line 351
  20. lemma OAI.SplitTangent.TangentSplitting.coordinateProjector_swap line 390
  21. lemma OAI.HolomorphicFrobenius.InvolutiveAt.congr line 407
  22. theorem OAI.SplitTangent.TangentSplitting.bracketTensor_eq_zero_of_integrable_firstAlternative line 446
  23. instance OAI.SplitTangent.FormalCauchy.(instance at line 520) line 520
  24. theorem OAI.SplitTangent.ProjectiveEmbedding.cone_local_equationsAlternative line 549
  25. theorem OAI.SplitTangent.ProjectiveEmbedding.exists_local_liftAlternative line 613
  26. def OAI.HolomorphicFlow.pointwiseMultilinear line 783
  27. lemma OAI.HolomorphicFlow.pointwiseMultilinear_bound line 802
  28. def OAI.HolomorphicFlow.pointwiseCoefficient line 813
  29. theorem OAI.HolomorphicFlow.pointwiseCoefficient_apply line 818
  30. lemma OAI.HolomorphicFlow.pointwiseCoefficient_norm line 822
  31. def OAI.HolomorphicFlow.pointwiseSeries line 827
  32. lemma OAI.HolomorphicFlow.pointwiseSeries_radius line 830
  33. lemma OAI.HolomorphicFlow.pointwiseSeries_sum line 845
  34. theorem OAI.HolomorphicFlow.exists_analytic_path_map line 856
  35. abbrev OAI.HolomorphicFlow.Time line 881
  36. def OAI.HolomorphicFlow.constantPath line 885
  37. lemma OAI.HolomorphicFlow.constantPath_apply line 892
  38. def OAI.HolomorphicFlow.extendPath line 895
  39. lemma OAI.HolomorphicFlow.extendPath_continuous line 898
  40. lemma OAI.HolomorphicFlow.extendPath_val line 902
  41. def OAI.HolomorphicFlow.volterraPath line 906
  42. lemma OAI.HolomorphicFlow.volterraPath_bound line 917
  43. def OAI.HolomorphicFlow.volterraLinear line 928
  44. def OAI.HolomorphicFlow.volterra line 945
  45. lemma OAI.HolomorphicFlow.volterra_apply line 948
  46. lemma OAI.HolomorphicFlow.volterra_zero line 951
  47. lemma OAI.HolomorphicFlow.volterra_hasDerivAt line 954
  48. theorem OAI.HolomorphicFlow.analytic_implicit_of_snd line 973
  49. theorem OAI.HolomorphicFlow.analytic_integral_equation_unique line 1044
  50. theorem OAI.HolomorphicFlow.analytic_integral_equation line 1109
  51. def OAI.HolomorphicFlow.PathEquation line 1126
  52. lemma OAI.HolomorphicFlow.pathEquation_iff line 1129
  53. theorem OAI.HolomorphicFlow.exists_analytic_paths line 1139
  54. lemma OAI.HolomorphicFlow.PathEquation.zero line 1159
  55. lemma OAI.HolomorphicFlow.PathEquation.at_zero_time line 1166
  56. lemma OAI.HolomorphicFlow.eventually_pointwise line 1184
  57. lemma OAI.HolomorphicFlow.eventually_continuous_integrand line 1194
  58. def OAI.HolomorphicFlow.realizedPath line 1206
  59. lemma OAI.HolomorphicFlow.PathEquation.realized_eq line 1210
  60. lemma OAI.HolomorphicFlow.realizedPath_hasDerivAt line 1215
  61. def OAI.HolomorphicFlow.scaleTime line 1231
  62. def OAI.HolomorphicFlow.rescale line 1236
  63. lemma OAI.HolomorphicFlow.rescale_apply line 1242
  64. lemma OAI.HolomorphicFlow.rescale_norm line 1246
  65. def OAI.HolomorphicFlow.scaleParameter line 1249
  66. lemma OAI.HolomorphicFlow.scaleParameter_norm line 1252
  67. lemma OAI.HolomorphicFlow.extendPath_rescale line 1258
  68. lemma OAI.HolomorphicFlow.PathEquation.rescale line 1266
  69. theorem OAI.HolomorphicFlow.eventually_rescale line 1295
  70. abbrev OAI.HolomorphicFlow.finalTime line 1323
  71. def OAI.HolomorphicFlow.endpoint line 1325
  72. lemma OAI.HolomorphicFlow.endpoint_analytic line 1329
  73. lemma OAI.HolomorphicFlow.rescale_endpoint_derivative line 1335
  74. lemma OAI.HolomorphicFlow.rescale_endpoint_time_derivative line 1373
  75. lemma OAI.HolomorphicFlow.eq_of_nonzero_time line 1387
  76. theorem OAI.HolomorphicFlow.exists_analytic_flow line 1401
  77. def OAI.HolomorphicFlow.initialDerivative line 1445
  78. lemma OAI.HolomorphicFlow.initialDerivative_apply line 1449
  79. lemma OAI.HolomorphicFlow.flow_initial_derivative line 1455
  80. def OAI.HolomorphicFlow.transverseParameters line 1481
  81. lemma OAI.HolomorphicFlow.transverseParameters_apply line 1486
  82. theorem OAI.HolomorphicFlow.exists_normalized_flow_box line 1491
  83. lemma OAI.HolomorphicFlow.norm_real_smul_le line 1542
  84. theorem OAI.HolomorphicFlow.ode_unique_germ line 1548
  85. theorem OAI.HolomorphicFlow.ode_unique_parameter_germ line 1590
  86. lemma OAI.HolomorphicFlow.analytic_fderiv line 1648
  87. lemma OAI.HolomorphicFlow.variational_equation_at line 1654
  88. def OAI.HolomorphicFlow.jetField line 1678
  89. lemma OAI.HolomorphicFlow.jetField_analytic line 1681
  90. lemma OAI.HolomorphicFlow.initial_spatial_derivative line 1688
  91. theorem OAI.HolomorphicFlow.flow_preserves_commuting line 1704
  92. def OAI.HolomorphicFrobenius.graphField line 1769
  93. def OAI.HolomorphicFrobenius.graphSpace line 1772
  94. lemma OAI.HolomorphicFrobenius.mem_graphSpace line 1776
  95. lemma OAI.HolomorphicFrobenius.graphField_analytic line 1786
  96. lemma OAI.HolomorphicFrobenius.graphField_fderiv_fst line 1791
  97. lemma OAI.HolomorphicFrobenius.graphField_commute line 1802
  98. def OAI.HolomorphicFrobenius.horizontalProjection line 1823
  99. lemma OAI.HolomorphicFrobenius.horizontalProjection_apply line 1827
  100. def OAI.HolomorphicFrobenius.projectorStraightener line 1830
  101. lemma OAI.HolomorphicFrobenius.projectorStraightener_horizontal line 1834
  102. lemma OAI.HolomorphicFrobenius.projector_straightener_intertwine line 1841
  103. def OAI.HolomorphicFrobenius.firstBlock line 1854
  104. def OAI.HolomorphicFrobenius.secondBlock line 1857
  105. def OAI.HolomorphicFrobenius.projectorGraph line 1860
  106. lemma OAI.HolomorphicFrobenius.firstBlock_horizontal line 1864
  107. lemma OAI.HolomorphicFrobenius.secondBlock_horizontal line 1868
  108. lemma OAI.HolomorphicFrobenius.projectorGraph_horizontal line 1872
  109. lemma OAI.HolomorphicFrobenius.firstBlock_analytic line 1876
  110. lemma OAI.HolomorphicFrobenius.secondBlock_analytic line 1881
  111. lemma OAI.HolomorphicFrobenius.projectorGraph_analytic line 1886
  112. lemma OAI.HolomorphicFrobenius.projector_range_eq_graph line 1897
  113. theorem OAI.HolomorphicFrobenius.exists_projector_graph line 1939
  114. abbrev OAI.HolomorphicFrobenius.FrameModel line 1967
  115. def OAI.HolomorphicFrobenius.horizontalBasis line 1969
  116. def OAI.HolomorphicFrobenius.timeCoordinate line 1971
  117. lemma OAI.HolomorphicFrobenius.timeCoordinate_apply line 1975
  118. lemma OAI.HolomorphicFrobenius.timeCoordinate_basis line 1979
  119. lemma OAI.HolomorphicFrobenius.flow_comp_fderiv line 1983
  120. lemma OAI.HolomorphicFrobenius.flow_time_fderiv line 1992
  121. theorem OAI.HolomorphicFrobenius.exists_partial_frame_coordinates line 2003
  122. lemma OAI.HolomorphicFrobenius.sum_horizontalBasis line 2077
  123. lemma OAI.HolomorphicFrobenius.eq_id_of_basis_and_transverse line 2085
  124. lemma OAI.HolomorphicFrobenius.frame_initial_derivative line 2098
  125. theorem OAI.HolomorphicFrobenius.exists_commuting_frame_chart_strong line 2118
  126. theorem OAI.HolomorphicFrobenius.exists_commuting_frame_chart line 2143
  127. theorem OAI.HolomorphicFrobenius.exists_graph_frobenius_chart_strong line 2158
  128. theorem OAI.HolomorphicFrobenius.exists_graph_frobenius_chart line 2190
  129. lemma OAI.HolomorphicFrobenius.image_horizontal_eq_graph line 2221
  130. theorem OAI.HolomorphicFrobenius.exists_normalized_projector_frobenius_strong line 2242
  131. theorem OAI.HolomorphicFrobenius.exists_normalized_projector_frobenius line 2277
  132. def OAI.HolomorphicFrobenius.affineCoordinates line 2303
  133. def OAI.HolomorphicFrobenius.affineUncoordinates line 2304
  134. def OAI.HolomorphicFrobenius.changedProjector line 2306
  135. def OAI.HolomorphicFrobenius.liftedField line 2310
  136. lemma OAI.HolomorphicFrobenius.affineCoordinates_uncoordinates line 2314
  137. lemma OAI.HolomorphicFrobenius.affineUncoordinates_coordinates line 2319
  138. lemma OAI.HolomorphicFrobenius.affineCoordinates_hasFDerivAt line 2324
  139. lemma OAI.HolomorphicFrobenius.affineUncoordinates_hasFDerivAt line 2331
  140. lemma OAI.HolomorphicFrobenius.affineCoordinates_analytic line 2336
  141. lemma OAI.HolomorphicFrobenius.affineUncoordinates_analytic line 2341
  142. lemma OAI.HolomorphicFrobenius.liftedField_analytic line 2346
  143. lemma OAI.HolomorphicFrobenius.liftedField_hasFDerivAt line 2353
  144. lemma OAI.HolomorphicFrobenius.liftedField_bracket line 2361
  145. lemma OAI.HolomorphicFrobenius.mem_changedProjector_range_iff line 2371
  146. lemma OAI.HolomorphicFrobenius.changedProjector_analytic line 2387
  147. theorem OAI.HolomorphicFrobenius.InvolutiveAt.changed line 2398
  148. def OAI.HolomorphicFrobenius.projectorDecomposition line 2438
  149. lemma OAI.HolomorphicFrobenius.projectorDecomposition_apply line 2464
  150. lemma OAI.HolomorphicFrobenius.projectorDecomposition_project line 2469
  151. def OAI.HolomorphicFrobenius.projectorCoordinates line 2479
  152. lemma OAI.HolomorphicFrobenius.projectorCoordinates_project line 2486
  153. lemma OAI.HolomorphicFrobenius.projectorCoordinates_project_symm line 2491
  154. lemma OAI.HolomorphicFrobenius.localHomeomorph_fderiv_left_inverse line 2507
  155. lemma OAI.HolomorphicFrobenius.localHomeomorph_fderiv_right_inverse line 2517
  156. theorem OAI.HolomorphicFrobenius.exists_normalized_leaf_submersion line 2529
  157. lemma OAI.HolomorphicFrobenius.changedProjector_idempotent line 2602
  158. theorem OAI.HolomorphicFrobenius.exists_leaf_submersion line 2616
  159. lemma OAI.HolomorphicFrobenius.range_complementary_projector line 2679
  160. lemma OAI.HolomorphicFrobenius.complementary_projector_idempotent line 2692
  161. lemma OAI.HolomorphicFrobenius.complementary_quotients_bijective line 2700
  162. lemma OAI.HolomorphicFrobenius.image_range_projector_of_quotients line 2744
  163. lemma OAI.HolomorphicFrobenius.image_kernel_projector_of_quotients line 2774
  164. abbrev OAI.HolomorphicFrobenius.FirstQuotient line 2813
  165. abbrev OAI.HolomorphicFrobenius.SecondQuotient line 2815
  166. theorem OAI.HolomorphicFrobenius.exists_local_product_chart line 2820
  167. theorem OAI.SplitTangent.TangentSplitting.coordinateProjector_involutiveAlternative line 2902
  168. lemma OAI.SplitTangent.LeadingJet.composition_leading line 2973
  169. def OAI.SplitTangent.LeadingJet.cut line 2992
  170. lemma OAI.SplitTangent.LeadingJet.cut_hasFPowerSeries line 2995
  171. theorem OAI.SplitTangent.LeadingJet.iteratedFDeriv_comp_of_lower_zero line 3020
  172. lemma OAI.SplitTangent.LeadingJet.iteratedFDeriv_smul_zeroAlternative line 3052
  173. def OAI.SplitTangent.HorizontalJet.value line 3094
  174. lemma OAI.SplitTangent.HorizontalJet.slice_analytic line 3100
  175. lemma OAI.SplitTangent.HorizontalJet.value_eq_zero_iff line 3105
  176. lemma OAI.SplitTangent.HorizontalJet.value_congr line 3116
  177. lemma OAI.SplitTangent.HorizontalJet.value_smul line 3125
  178. theorem OAI.SplitTangent.HorizontalJet.value_comp line 3137
  179. theorem OAI.SplitTangent.HorizontalJet.eventually_zero_of_all_zero line 3185
  180. lemma OAI.SplitTangent.HorizontalJet.iterated_comp_linear line 3216
  181. lemma OAI.SplitTangent.HorizontalJet.value_eq_total line 3231
  182. theorem OAI.SplitTangent.HorizontalJet.analytic_value line 3257
  183. lemma OAI.SplitTangent.HorizontalJet.value_symmetric line 3270
  184. lemma OAI.SplitTangent.HorizontalJet.analytic_parameter_value line 3278
  185. theorem OAI.SplitTangent.HorizontalJet.analytic_valueAlternative line 3323
  186. theorem OAI.SplitTangent.PositiveTensor.contraction_order line 3349
  187. theorem OAI.SplitTangent.PositiveTensor.lineSection_zero_of_order line 3378
  188. theorem OAI.SplitTangent.PositiveTensor.lineSection_zero_of_contraction line 3390
  189. lemma OAI.MvPolynomial.contMDiffAt_eval_comp line 3449
  190. lemma OAI.MvPolynomial.IsHomogeneous.eval_scale line 3470
  191. def OAI.AnalyticGermContinuation.LocallyAnalyticZeroSet line 3496
  192. lemma OAI.AnalyticGermContinuation.closure_interior_subset line 3500
  193. theorem OAI.AnalyticGermContinuation.propagate line 3518
  194. lemma OAI.UniformPlaqueSlices.connected_rectangle line 3559
  195. theorem OAI.UniformPlaqueSlices.exists_slices line 3568
  196. lemma OAI.HolomorphicDeterminant.contMDiffAt_det line 3606
  197. lemma OAI.FiniteSampling.exists_nonsingular_samples line 3627
  198. lemma OAI.FiniteSampling.relation_iff_det_zero line 3656
  199. theorem OAI.SplitTangent.ProjectorSpanning.eventually_range_eq line 3693
  200. theorem OAI.SplitTangent.ProjectorSpanning.multilinear_zero_of_basis_range line 3718
  201. abbrev OAI.SplitTangent.SymmetricIndex.Sorted line 3753
  202. def OAI.SplitTangent.SymmetricIndex.toSym line 3755
  203. theorem OAI.SplitTangent.SymmetricIndex.toSym_injective line 3758
  204. theorem OAI.SplitTangent.SymmetricIndex.card_le line 3766
  205. def OAI.SplitTangent.SymmetricIndex.sort line 3770
  206. theorem OAI.SplitTangent.SymmetricIndex.zero_of_sorted line 3774
  207. abbrev OAI.SeparatedQuotientFiltration.zeroPart line 3816
  208. abbrev OAI.SeparatedQuotientFiltration.Space line 3817
  209. abbrev OAI.SeparatedQuotientFiltration.stage line 3818
  210. lemma OAI.SeparatedQuotientFiltration.zeroPart_le line 3820
  211. lemma OAI.SeparatedQuotientFiltration.stage_antitone line 3822
  212. def OAI.SeparatedQuotientFiltration.project line 3824
  213. lemma OAI.SeparatedQuotientFiltration.project_surjective line 3829
  214. lemma OAI.SeparatedQuotientFiltration.project_zero_iff line 3834
  215. lemma OAI.SeparatedQuotientFiltration.separated line 3839
  216. lemma OAI.SeparatedQuotientFiltration.descends line 3853
  217. def OAI.SeparatedQuotientFiltration.leading line 3857
  218. lemma OAI.SeparatedQuotientFiltration.leading_project line 3861
  219. lemma OAI.SeparatedQuotientFiltration.leading_kernel line 3865
  220. lemma OAI.AnalyticFlatFamily.germ_zero_of_derivatives line 3902
  221. theorem OAI.AnalyticFlatFamily.joint_germ_zero line 3922
  222. lemma OAI.PolynomialCoefficientGerms.coefficients_zero line 3960
  223. theorem OAI.PolynomialCoefficientGerms.coefficient_germs line 3976
  224. def OAI.LinearKernelDimension.factor line 4005
  225. lemma OAI.LinearKernelDimension.factor_apply line 4009
  226. theorem OAI.LinearKernelDimension.finite_and_bound line 4016
  227. lemma OAI.PolynomialGrowthArithmetic.cancel_graph_dimension line 4035
  228. lemma OAI.PolynomialGrowthArithmetic.box_exceeds line 4047
  229. def OAI.BoxMonomials.homogeneousAlternative line 4077
  230. def OAI.BoxMonomials.homogeneousForms line 4096
  231. lemma OAI.BoxMonomials.eval_homogeneousForms line 4110
  232. lemma OAI.RectangularInverse.exists_continuous_left_inverse line 4157
  233. lemma OAI.RectangularInverse.triangular_bijective line 4165
  234. theorem OAI.RectangularInverse.exists_chart line 4188
  235. lemma OAI.PolynomialSpecialization.eval_analyticAtAlternative line 4237
  236. theorem OAI.PolynomialSpecialization.finite_transversal line 4268
  237. theorem OAI.HolomorphicLocalDiffeomorph.of_analytic_partial_homeomorphAlternative line 4356
  238. theorem OAI.HolomorphicLocalDiffeomorph.congr_eventuallyAlternative line 4392
  239. lemma OAI.HolomorphicLocalDiffeomorph.map_nhds_of_surjective_mfderiv line 4424
  240. lemma OAI.HolomorphicLocalDiffeomorph.isOpenMap_of_surjective_mfderiv line 4465
  241. theorem OAI.SplitTangent.RationallyConnected.exists_submersive_family_in_openAlternative line 4486
  242. lemma OAI.FiniteOpenMaps.constantCardLocus_isOpenAlternative line 4677
  243. lemma OAI.FiniteOpenMaps.locally_injective_of_card_constantAlternative line 4700
  244. lemma OAI.SplitTangent.holomorphicAt_tangentMapAlternative line 4842