DividedFamilies.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Divided analytic families, moving centres, and specialization jets; Local graph representation of inverse normal charts

def OAI.Nagata.Workers.W28.normalFamilyArgument line 18
Source documentation
Actual argument of the inverse normal chart in parameter and fiber variables.
```
def normalFamilyArgument (z : ℂ × ComplexPlane) : ComplexPlane := (z.2.1, z.1 * z.2.2)
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
def OAI.Nagata.Workers.W28.dividedAnalyticFamily line 22
Source documentation
Finite divided normal family; every exponent is a natural number, so the formula defines an actual function at the central parameter zero.
```
def dividedAnalyticFamily (I : Finset ℕ) (j : ℕ → ℕ)
    (R : ℕ → MvPolynomial (Fin 2) ℂ) (u : ℕ) (κ : ComplexPlane → ComplexPlane)
    (z : ℂ × ComplexPlane) : ℂ :=
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
theorem OAI.Nagata.Workers.W28.normalFamilyArgument_analyticAt line 28
theorem OAI.Nagata.Workers.W28.dividedAnalyticFamily_analyticAt line 38
Source documentation
Joint holomorphy of the actual divided normal family follows from actual holomorphy of the inverse chart at its argument.
```
theorem dividedAnalyticFamily_analyticAt
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (u : ℕ) (κ : ComplexPlane → ComplexPlane) (z : ℂ × ComplexPlane)
    (hκ : AnalyticAt ℂ κ (normalFamilyArgument z)) :
    AnalyticAt ℂ (dividedAnalyticFamily I j R u κ) z := by
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.normalFamilyArgument, OAI.Nagata.Workers.W28.dividedAnalyticFamily

theorem OAI.Nagata.Workers.W28.originalFamily_eq_power_mul_divided line 53

Source documentation

Exact scalar factorization of the original G-adic family in normal coordinates.

theorem originalFamily_eq_power_mul_divided
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (G : MvPolynomial (Fin 2) ℂ) (κ : ComplexPlane → ComplexPlane)
    (z : ℂ × ComplexPlane)
    (hG : planePolynomialEval G (κ (normalFamilyArgument z)) = z.1 * z.2.2) :
    (∑ α ∈ I, z.1 ^ α * planePolynomialEval G (κ (normalFamilyArgument z)) ^ j α *
      planePolynomialEval (R α) (κ (normalFamilyArgument z))) =
      z.1 ^ u * dividedAnalyticFamily I j R u κ z := by
…

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

theorem OAI.Nagata.Workers.W28.dividedAnalyticFamily_zero line 73

Source documentation

The actual central value is the initial normal polynomial with the remainder polynomials restricted through the chart at normal coordinate zero.

theorem dividedAnalyticFamily_zero
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (κ : ComplexPlane → ComplexPlane) (q : ComplexPlane) :
    dividedAnalyticFamily I j R u κ (0, q) =
      ∑ α ∈ I.filter (fun α => α + j α = u),
        q.2 ^ j α * planePolynomialEval (R α) (κ (q.1, 0)) := by
…

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

def OAI.Nagata.Workers.W28.dividedNormalCoordinate line 103
Source documentation
The actual divided normal coordinate, extended at zero by the derivative.
```
def dividedNormalCoordinate (G : ComplexPlane → ℂ) (L : ComplexPlane →L[ℂ] ℂ)
    (p V : ComplexPlane) : ℂ → ℂ :=
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
def OAI.Nagata.Workers.W28.dividedNormalCenter line 108
Source documentation
Actual center in the rescaled normal chart for an affine moving point.
```
def dividedNormalCenter (G : ComplexPlane → ℂ) (L : ComplexPlane →L[ℂ] ℂ)
    (p V : ComplexPlane) (s : ℂ) : ComplexPlane :=
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
theorem OAI.Nagata.Workers.W28.dividedNormalCenter_zero line 112
theorem OAI.Nagata.Workers.W28.dividedNormalCenter_continuousAt line 117
theorem OAI.Nagata.Workers.W28.scale_dividedNormalCenter line 127
Source documentation
Away from zero the rescaled divided center is exactly the actual normal chart image of the moving affine point.
```
theorem scale_dividedNormalCenter
    (G : MvPolynomial (Fin 2) ℂ) (L : ComplexPlane →L[ℂ] ℂ)
    (p V : ComplexPlane) (s : ℂ) (hs : s ≠ 0) :
    analyticNormalScale s (dividedNormalCenter (planePolynomialEval G) L p V s) =
      polynomialNormalCoordinates G (p + s • V) := by
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.analyticNormalScale, OAI.Nagata.Workers.W28.dividedNormalCenter, OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.Workers.W28.polynomialNormalCoordinates

theorem OAI.Nagata.Workers.W28.inverse_at_dividedNormalCenter line 137

Source documentation

The actual moving point is recovered by the inverse chart at the divided normal center, wherever that moving point lies in the chart source.

theorem inverse_at_dividedNormalCenter
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (L : ComplexPlane →L[ℂ] ℂ) (p V : ComplexPlane) (s : ℂ) (hs : s ≠ 0)
    (hsource : p + s • V ∈ e.source) :
    e.symm (analyticNormalScale s (dividedNormalCenter (planePolynomialEval G) L p V s)) =
      p + s • V := by
…

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

theorem OAI.Nagata.Workers.W28.eventually_divided_center_chart_conditions line 161

Source documentation

Actual affine motions remain inside the chosen normal chart near zero, and their rescaled center lies in the inverse chart's analytic neighborhood.

theorem eventually_divided_center_chart_conditions
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (L : ComplexPlane →L[ℂ] ℂ) (p V : ComplexPlane)
    (hp : p ∈ e.source) (hi : AnalyticAt ℂ e.symm (e p)) :
    ∀ᶠ s : ℂ in 𝓝 0, s ≠ 0 →
      p + s • V ∈ e.source ∧
      analyticNormalScale s (dividedNormalCenter (planePolynomialEval G) L p V s) ∈ e.target ∧
      AnalyticAt ℂ e.symm
        (analyticNormalScale s (dividedNormalCenter (planePolynomialEval G) L p V s)) := by
…

def OAI.Nagata.Workers.W28.factoredPlaneFamily line 204
Source documentation
The actual polynomial in the original affine plane at fixed parameter s, with its finite G-adic coefficient decomposition made explicit.
```
def factoredPlaneFamily (I : Finset ℕ) (j : ℕ → ℕ)
    (R : ℕ → MvPolynomial (Fin 2) ℂ) (G : MvPolynomial (Fin 2) ℂ)
    (s : ℂ) : MvPolynomial (Fin 2) ℂ :=
…
```
theorem OAI.Nagata.Workers.W28.eval_factoredPlaneFamily line 209

theorem OAI.Nagata.Workers.W28.factored_family_order_implies_divided_order line 219

Source documentation

Actual polynomial multiplicity of the moving plane curve transfers to the divided holomorphic family for every nonzero parameter. All chart conditions are local statements about the actual inverse map at the actual point.

theorem factored_family_order_implies_divided_order
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (s : ℂ) (hs : s ≠ 0) (q : ComplexPlane) (m : ℕ)
    (htarget : analyticNormalScale s q ∈ e.target)
    (hei : AnalyticAt ℂ e.symm (analyticNormalScale s q))
    (hP : Nagata.AffineMultiplicity.orderAtLeast
      (fun i : Fin 2 => if i = 0 then (e.symm (analyticNormalScale s q)).1
        else (e.symm (analyticNormalScale s q)).2)
…

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

theorem OAI.Nagata.Workers.W28.normal_specialization_central_jets line 265

Source documentation

Local normal specialization for an actual finite polynomial family. The hypotheses assert its original ordinary ideal-power multiplicities along an affine motion. The conclusion asserts genuine central derivative jets; no analytic jet hypothesis or derivative-continuity assumption is supplied.

theorem normal_specialization_central_jets
    (I : Finset ℕ) (j : ℕ → ℕ) (R : ℕ → MvPolynomial (Fin 2) ℂ)
    (u : ℕ) (hmin : ∀ α ∈ I, u ≤ α + j α)
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (L : ComplexPlane →L[ℂ] ℂ) (p V : ComplexPlane)
    (hsource : p ∈ e.source) (hi : AnalyticAt ℂ e.symm (e p))
    (hG : HasFDerivAt (planePolynomialEval G) L p)
    (hp : planePolynomialEval G p = 0)
    (exceptional : Finset ℂ) (m : ℕ)
    (horders : ∀ᶠ s : ℂ in 𝓝 0, s ∉ exceptional →
…

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

theorem OAI.Nagata.Workers.W28.inverse_normal_chart_eq_graph_locally line 332

Source documentation

A genuine local graph on G=0 is the zero-normal slice of the constructed normal chart, by its actual local inverse identity.

theorem inverse_normal_chart_eq_graph_locally
    (G : MvPolynomial (Fin 2) ℂ)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates G)
    (b : ℂ → ℂ) (ξ : ℂ) (hb : ContinuousAt b ξ)
    (hsource : (ξ, b ξ) ∈ e.source)
    (hG : ∀ᶠ z in 𝓝 ξ, planePolynomialEval G (z, b z) = 0) :
    ∀ᶠ z in 𝓝 ξ, e.symm (z, 0) = (z, b z) := by
…

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

theorem OAI.Nagata.Workers.W28.central_expression_eq_graph_locally line 349

Source documentation

The actual central expression in inverse normal coordinates agrees as a local function germ with the expression restricted to an actual graph on G=0.

theorem central_expression_eq_graph_locally
    (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) :
    (fun q : ComplexPlane => ∑ α ∈ I.filter (fun α => α + j α = u),
      q.2 ^ j α * planePolynomialEval (R α) (e.symm (q.1, 0))) =ᶠ[𝓝 (ξ, c)]
    (fun q : ComplexPlane => ∑ α ∈ I.filter (fun α => α + j α = u),
      q.2 ^ j α * planePolynomialEval (R α) (q.1, b q.1)) := by
…

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