GraphOrder.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Nested, parametric, and line order along normal graphs

theorem OAI.Nagata.Workers.W28.central_expression_analyticAt line 19

Source documentation

The selected central expression is an actual analytic function near any zero-normal point where the inverse chart is analytic.

theorem central_expression_analyticAt
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ) (u : ℕ)
    (κ : ComplexPlane → ComplexPlane) (ξ c : ℂ)
    (hκ : AnalyticAt ℂ κ (ξ, 0)) :
    AnalyticAt ℂ
      (fun q : ComplexPlane => ∑ α ∈ I.filter (fun α => α + j α = u),
        q.2 ^ j α * planePolynomialEval (R α) (κ (q.1, 0))) (ξ, c) := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.planePolynomialEval

theorem OAI.Nagata.Workers.W28.graph_expression_order_of_central_jets line 42

Source documentation

The actual central derivative conclusion implies actual analytic order for the graph-restricted polynomial expression, with the local graph equality proved from the normal chart rather than assumed as a representation field.

theorem graph_expression_order_of_central_jets
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ) (u : ℕ)
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (b : ℂ → ℂ) (ξ c : ℂ) (hb : ContinuousAt b ξ)
    (hsource : (ξ, b ξ) ∈ e.source)
    (hG : ∀ᶠ z in 𝓝 ξ, planePolynomialEval G (z, b z) = 0)
    (hi : AnalyticAt ℂ e.symm (ξ, 0)) (m : ℕ)
    (hjets : ∀ n < m, iteratedFDeriv ℂ n
      (fun q : ComplexPlane => ∑ α ∈ I.filter (fun α => α + j α = u),
        q.2 ^ j α * planePolynomialEval (R α) (e.symm (q.1, 0))) (ξ, c) = 0) :
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.planePolynomialEval

def OAI.Nagata.Workers.W28.selectedGraphPolynomial line 73
Source documentation
The actual normal polynomial with univariate graph-restricted coefficients.
```
def selectedGraphPolynomial (I : Finset ℕ) (j : ℕ → ℕ)
    (B : ℕ → Polynomial ℂ) (u : ℕ) : Polynomial (Polynomial ℂ) :=
…
```
theorem OAI.Nagata.Workers.W28.eval_selectedGraphPolynomial line 77

theorem OAI.Nagata.Workers.W28.selectedGraphPolynomial_order_of_graph_order line 85

Source documentation

The genuine local graph analytic order gives ordinary ideal-power multiplicity for its actual finite normal polynomial, via exact coefficient evaluation.

theorem selectedGraphPolynomial_order_of_graph_order
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (B : ℕ → Polynomial ℂ) (u : ℕ) (b : ℂ → ℂ) (ξ c : ℂ) (m : ℕ)
    (hR : ∀ α ∈ I.filter (fun α => α + j α = u), ∀ z : ℂ,
      planePolynomialEval (R α) (z, b z) = (B α).eval z)
    (horder : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

theorem OAI.Nagata.Workers.W28.map_selected_monomial_sum line 105

Source documentation

Coefficientwise restriction of the actual selected plane normal polynomial is literally the graph normal polynomial used above.

theorem map_selected_monomial_sum
    {A : Type*} [CommRing A] (φ : A →+* Polynomial ℂ)
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → A) (u : ℕ) :
    Polynomial.map φ
      (∑ α ∈ I.filter (fun α => α + j α = u), Polynomial.monomial (j α) (T α)) =
        selectedGraphPolynomial I j (fun α => φ (T α)) u := by
…

Mentions: OAI.Nagata.Workers.W28.selectedGraphPolynomial

theorem OAI.Nagata.Workers.W28.inverse_normal_chart_eq_parametric_curve line 126

Source documentation

An actual curve parametrization on G=0 agrees locally with the zero-normal slice of the normal chart. No inverse for the tangential parametrization is used.

theorem inverse_normal_chart_eq_parametric_curve
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (p : ℂ → ComplexPlane) (z₀ : ℂ) (hp : ContinuousAt p z₀)
    (hsource : p z₀ ∈ e.source)
    (hG : ∀ᶠ z in 𝓝 z₀, planePolynomialEval G (p z) = 0) :
    ∀ᶠ z in 𝓝 z₀, e.symm ((p z).1, 0) = p z := by
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.planePolynomialEval

def OAI.Nagata.Workers.W28.curveNormalParameter line 141
Source documentation
Actual reparametrization and homogeneous normal-fiber rescaling.
```
def curveNormalParameter (p : ℂ → ComplexPlane) (a : ℂ → ℂ) (k : ℕ)
    (q : ComplexPlane) : ComplexPlane := ((p q.1).1, q.2 / a q.1 ^ k)
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
theorem OAI.Nagata.Workers.W28.curveNormalParameter_analyticAt line 144

theorem OAI.Nagata.Workers.W28.parametric_frame_order_of_central_order line 157

Source documentation

Actual central normal order pulls back along an analytic curve and is preserved by multiplication with the actual homogeneous frame factor a(z)^d.

theorem parametric_frame_order_of_central_order
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (p : ℂ → ComplexPlane) (a : ℂ → ℂ) (d k : ℕ) (z₀ w₀ : ℂ)
    (hp : AnalyticAt ℂ p z₀) (ha : AnalyticAt ℂ a z₀) (ha0 : a z₀ ≠ 0)
    (hsource : p z₀ ∈ e.source)
    (hG : ∀ᶠ z in 𝓝 z₀, planePolynomialEval G (p z) = 0)
    (m : ℕ)
    (horder : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

theorem OAI.Nagata.Workers.W28.line_restricted_initial_order line 203

Source documentation

The actual selected homogeneous normal polynomial, restricted to a line, has ordinary surface multiplicity forced by the local normal specialization. All coefficient/frame identifications use the actual Z=1 chart homomorphism and actual homogeneous line-restriction homomorphism.

theorem line_restricted_initial_order
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ) (u : ℕ)
    (G : MvPolynomial (Fin 3) ℂ) (i ξ c : ℂ)
    (hline : Nagata.W04.ReducibleSquare.lineRestriction i G = 0)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) =
      polynomialNormalCoordinates (Nagata.W27.directChartHom (2 : Fin 3) G))
    (hsource : (ξ, i ^ 2 - i * ξ) ∈ e.source)
    (hi : AnalyticAt ℂ e.symm (ξ, 0)) (m : ℕ)
    (hjets : ∀ n < m, iteratedFDeriv ℂ n
      (fun q : ComplexPlane => ∑ α ∈ I.filter (fun α => α + j α = u),
        q.2 ^ j α * planePolynomialEval (Nagata.W27.directChartHom (2 : Fin 3) (T α))
…

Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.planePolynomialEval