OAI/Geometry/HypersurfaceGerms/Preparation.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional analytic inversion and convergent preparation of polynomial graph equations.

  1. abbrev OAI.AmbientMultiplicity.Preparation.V line 12
  2. abbrev OAI.AmbientMultiplicity.Preparation.proj line 13
  3. def OAI.AmbientMultiplicity.Preparation.high line 15
  4. def OAI.AmbientMultiplicity.Preparation.highL line 18
  5. lemma OAI.AmbientMultiplicity.Preparation.highL_apply line 21
  6. def OAI.AmbientMultiplicity.Preparation.polyMap line 27
  7. def OAI.AmbientMultiplicity.Preparation.tangent line 31
  8. lemma OAI.AmbientMultiplicity.Preparation.tangent_apply line 36
  9. lemma OAI.AmbientMultiplicity.Preparation.high_strict line 46
  10. lemma OAI.AmbientMultiplicity.Preparation.polyMap_strict line 53
  11. lemma OAI.AmbientMultiplicity.Preparation.polyMap_analytic line 71
  12. lemma OAI.AmbientMultiplicity.Preparation.tangent_injective line 91
  13. lemma OAI.AmbientMultiplicity.Preparation.analytic_inverse line 132
  14. theorem OAI.AmbientMultiplicity.Preparation.factor_coordinates line 149
  15. def OAI.AmbientMultiplicity.Preparation.lowPoly line 162
  16. def OAI.AmbientMultiplicity.Preparation.highPoly line 165
  17. def OAI.AmbientMultiplicity.Preparation.rootPoly line 168
  18. lemma OAI.AmbientMultiplicity.Preparation.coeff_highPoly line 171
  19. lemma OAI.AmbientMultiplicity.Preparation.coeff_monomial_mul_any line 178
  20. lemma OAI.AmbientMultiplicity.Preparation.coeff_factor line 183
  21. lemma OAI.AmbientMultiplicity.Preparation.factor_natDegree_lt line 195
  22. lemma OAI.AmbientMultiplicity.Preparation.factor_eq_ofFn line 206
  23. def OAI.AmbientMultiplicity.Preparation.CoeffAnalytic line 214
  24. lemma OAI.AmbientMultiplicity.Preparation.coeffAnalytic_const line 217
  25. lemma OAI.AmbientMultiplicity.Preparation.coeffAnalytic_C line 220
  26. lemma OAI.AmbientMultiplicity.Preparation.CoeffAnalytic.add line 228
  27. lemma OAI.AmbientMultiplicity.Preparation.CoeffAnalytic.sub line 234
  28. lemma OAI.AmbientMultiplicity.Preparation.CoeffAnalytic.mul line 240
  29. lemma OAI.AmbientMultiplicity.Preparation.CoeffAnalytic.pow line 249
  30. lemma OAI.AmbientMultiplicity.Preparation.polyMap_fixed line 255
  31. theorem OAI.AmbientMultiplicity.Preparation.prepare_polynomial line 273
  32. def OAI.AmbientMultiplicity.Preparation.q1 line 290
  33. def OAI.AmbientMultiplicity.Preparation.q2 line 292
  34. def OAI.AmbientMultiplicity.Preparation.psi line 293
  35. def OAI.AmbientMultiplicity.Preparation.graph0 line 296
  36. def OAI.AmbientMultiplicity.Preparation.graph1 line 297
  37. lemma OAI.AmbientMultiplicity.Preparation.graph0_analytic line 299
  38. lemma OAI.AmbientMultiplicity.Preparation.graph1_analytic line 307
  39. lemma OAI.AmbientMultiplicity.Preparation.graph0_degree line 317
  40. lemma OAI.AmbientMultiplicity.Preparation.graph1_degree line 321
  41. lemma OAI.AmbientMultiplicity.Preparation.graph0_specialization line 325
  42. lemma OAI.AmbientMultiplicity.Preparation.graph1_specialization line 329
  43. theorem OAI.AmbientMultiplicity.Preparation.prepare_graph0 line 334
  44. theorem OAI.AmbientMultiplicity.Preparation.prepare_graph1 line 345
  45. def OAI.AmbientMultiplicity.Preparation.coeff0 line 357
  46. def OAI.AmbientMultiplicity.Preparation.coeff1 line 358
  47. lemma OAI.AmbientMultiplicity.Preparation.coeff0_spec line 360
  48. lemma OAI.AmbientMultiplicity.Preparation.coeff1_spec line 363
  49. lemma OAI.AmbientMultiplicity.Preparation.eval_rootPoly line 367
  50. lemma OAI.AmbientMultiplicity.Preparation.eval_highPoly line 371
  51. lemma OAI.AmbientMultiplicity.Preparation.analytic_rootPoly line 375
  52. lemma OAI.AmbientMultiplicity.Preparation.analytic_highPoly line 384
  53. def OAI.AmbientMultiplicity.Preparation.base3 line 392
  54. def OAI.AmbientMultiplicity.Preparation.root0 line 394
  55. def OAI.AmbientMultiplicity.Preparation.root1 line 395
  56. def OAI.AmbientMultiplicity.Preparation.unit0 line 396
  57. def OAI.AmbientMultiplicity.Preparation.unit1 line 397
  58. def OAI.AmbientMultiplicity.Preparation.r0 line 399
  59. def OAI.AmbientMultiplicity.Preparation.r1 line 400
  60. def OAI.AmbientMultiplicity.Preparation.u0 line 401
  61. def OAI.AmbientMultiplicity.Preparation.u1 line 402
  62. lemma OAI.AmbientMultiplicity.Preparation.r0_analytic line 404
  63. lemma OAI.AmbientMultiplicity.Preparation.r1_analytic line 409
  64. lemma OAI.AmbientMultiplicity.Preparation.u0_analytic line 414
  65. lemma OAI.AmbientMultiplicity.Preparation.u1_analytic line 419
  66. lemma OAI.AmbientMultiplicity.Preparation.root0_at_base_zero line 425
  67. lemma OAI.AmbientMultiplicity.Preparation.root1_at_base_zero line 433
  68. lemma OAI.AmbientMultiplicity.Preparation.r0_zero line 442
  69. lemma OAI.AmbientMultiplicity.Preparation.r1_zero line 443
  70. lemma OAI.AmbientMultiplicity.Preparation.u0_zero line 444
  71. lemma OAI.AmbientMultiplicity.Preparation.u1_zero line 449
  72. lemma OAI.AmbientMultiplicity.Preparation.graph0_factor line 455
  73. lemma OAI.AmbientMultiplicity.Preparation.graph1_factor line 461
  74. lemma OAI.AmbientMultiplicity.Preparation.strict_mul_vanishing line 468
  75. lemma OAI.AmbientMultiplicity.Preparation.graph0_deriv line 476
  76. lemma OAI.AmbientMultiplicity.Preparation.graph1_deriv line 496
  77. lemma OAI.AmbientMultiplicity.Preparation.derivative_unit_factor line 514
  78. lemma OAI.AmbientMultiplicity.Preparation.r0_deriv line 526
  79. lemma OAI.AmbientMultiplicity.Preparation.r1_deriv line 528
  80. def OAI.AmbientMultiplicity.Preparation.rescale line 532
  81. def OAI.AmbientMultiplicity.Preparation.ambient0 line 535
  82. def OAI.AmbientMultiplicity.Preparation.ambient1 line 537
  83. lemma OAI.AmbientMultiplicity.Preparation.ambient0_zero line 540
  84. lemma OAI.AmbientMultiplicity.Preparation.ambient1_zero line 542
  85. lemma OAI.AmbientMultiplicity.Preparation.ambient0_analytic line 545
  86. lemma OAI.AmbientMultiplicity.Preparation.ambient1_analytic line 557
  87. lemma OAI.AmbientMultiplicity.Preparation.yz_deriv line 571
  88. lemma OAI.AmbientMultiplicity.Preparation.ambient0_deriv line 577
  89. lemma OAI.AmbientMultiplicity.Preparation.ambient1_deriv line 590
  90. lemma OAI.AmbientMultiplicity.Preparation.inverse_map_analytic line 605
  91. def OAI.AmbientMultiplicity.Preparation.ambientEquiv0 line 617
  92. def OAI.AmbientMultiplicity.Preparation.ambientEquiv1 line 619
  93. lemma OAI.AmbientMultiplicity.Preparation.ambientEquiv0_apply line 622
  94. lemma OAI.AmbientMultiplicity.Preparation.ambientEquiv1_apply line 623
  95. lemma OAI.AmbientMultiplicity.Preparation.ambientEquiv0_source line 624
  96. lemma OAI.AmbientMultiplicity.Preparation.ambientEquiv1_source line 626
  97. lemma OAI.AmbientMultiplicity.Preparation.inverse0_zero line 628
  98. lemma OAI.AmbientMultiplicity.Preparation.inverse1_zero line 631
  99. lemma OAI.AmbientMultiplicity.Preparation.inverse0_analytic line 634
  100. lemma OAI.AmbientMultiplicity.Preparation.inverse1_analytic line 637
  101. def OAI.AmbientMultiplicity.Preparation.embed0 line 641
  102. def OAI.AmbientMultiplicity.Preparation.embed1 line 642
  103. def OAI.AmbientMultiplicity.Preparation.chart0 line 644
  104. def OAI.AmbientMultiplicity.Preparation.chart1 line 645
  105. lemma OAI.AmbientMultiplicity.Preparation.chart0_zero line 646
  106. lemma OAI.AmbientMultiplicity.Preparation.chart1_zero line 647
  107. lemma OAI.AmbientMultiplicity.Preparation.chart0_analytic line 648
  108. lemma OAI.AmbientMultiplicity.Preparation.chart1_analytic line 651
  109. lemma OAI.AmbientMultiplicity.Preparation.chart0_eq line 654
  110. lemma OAI.AmbientMultiplicity.Preparation.chart1_eq line 659
  111. lemma OAI.AmbientMultiplicity.Preparation.chart0_coordinates line 665
  112. lemma OAI.AmbientMultiplicity.Preparation.chart1_coordinates line 677
  113. lemma OAI.AmbientMultiplicity.Preparation.chart0_implicit line 690
  114. lemma OAI.AmbientMultiplicity.Preparation.chart1_implicit line 704
  115. def OAI.AmbientMultiplicity.Preparation.eliminated0 line 720
  116. def OAI.AmbientMultiplicity.Preparation.eliminated1 line 721
  117. lemma OAI.AmbientMultiplicity.Preparation.eliminated0_analytic line 722
  118. lemma OAI.AmbientMultiplicity.Preparation.eliminated1_analytic line 724
  119. lemma OAI.AmbientMultiplicity.Preparation.eliminated0_zero line 726
  120. lemma OAI.AmbientMultiplicity.Preparation.eliminated1_zero line 727
  121. def OAI.AmbientMultiplicity.Preparation.perturbation line 729
  122. lemma OAI.AmbientMultiplicity.Preparation.perturbation_analytic line 730
  123. def OAI.AmbientMultiplicity.Preparation.f5 line 734
  124. def OAI.AmbientMultiplicity.Preparation.f4 line 736
  125. lemma OAI.AmbientMultiplicity.Preparation.f5_analytic line 739
  126. lemma OAI.AmbientMultiplicity.Preparation.f4_analytic line 744
  127. lemma OAI.AmbientMultiplicity.Preparation.f5_zero line 749
  128. lemma OAI.AmbientMultiplicity.Preparation.f4_zero line 751
  129. lemma OAI.AmbientMultiplicity.Preparation.f5_source line 756
  130. lemma OAI.AmbientMultiplicity.Preparation.f4_source line 763
  131. lemma OAI.AmbientMultiplicity.Preparation.chart0_on_hypersurface line 771
  132. lemma OAI.AmbientMultiplicity.Preparation.chart1_on_hypersurface line 776