HomogeneousOrder.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous multiplicity in normal frames and swapped charts; Homogeneous smooth curve charts

def OAI.Nagata.Workers.W28.normalizedCurvePoint line 17
Source documentation
Actual affine chart coordinates of a homogeneous analytic parametrization.
```
def normalizedCurvePoint (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z : ℂ) : ComplexPlane :=
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane
theorem OAI.Nagata.Workers.W28.normalizedCurvePoint_analyticAt line 20

theorem OAI.Nagata.Workers.W28.normalizedCurvePoint_equation line 28

Source documentation

The actual homogeneous curve equation implies the actual affine chart equation.

theorem normalizedCurvePoint_equation
    (G : MvPolynomial (Fin 3) ℂ) (k : ℕ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z : ℂ)
    (hc : X c z ≠ 0) (hzero : MvPolynomial.eval (fun a => X a z) G = 0) :
    planePolynomialEval (Nagata.W27.directChartHom c G) (normalizedCurvePoint X c z) = 0 := by
…

Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint

theorem OAI.Nagata.Workers.W28.normalizedCurvePoint_equation_locally line 52

Source documentation

The homogeneous-to-affine equation holds on an actual neighborhood where the chosen analytic homogeneous coordinate stays nonzero.

theorem normalizedCurvePoint_equation_locally
    (G : MvPolynomial (Fin 3) ℂ) (k : ℕ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ : ℂ)
    (ha : ContinuousAt (X c) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0) :
    ∀ᶠ z in 𝓝 z₀, planePolynomialEval (Nagata.W27.directChartHom c G)
      (normalizedCurvePoint X c z) = 0 := by
…

Mentions: OAI.Nagata.Workers.W28.planePolynomialEval, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint

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

theorem OAI.Nagata.Workers.W28.homogeneous_normal_order_of_central_order line 92

Source documentation

Central normal order implies actual homogeneous polynomial order on an analytic parametrized curve, with the exact variable degree-d frame factor.

theorem homogeneous_normal_order_of_central_order
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ w₀ : ℂ)
    (hX : ∀ a, AnalyticAt ℂ (X a) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates (Nagata.W27.directChartHom c G))
    (hsource : normalizedCurvePoint X c z₀ ∈ e.source) (m : ℕ)
    (horder : HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

theorem OAI.Nagata.Workers.W28.analyticAt_curve_swap line 133
Source documentation
Swapping actual affine coordinates preserves analyticity of a curve.
```
theorem analyticAt_curve_swap (p : ℂ → ComplexPlane) (z₀ : ℂ)
    (hp : AnalyticAt ℂ p z₀) : AnalyticAt ℂ (fun z => (p z).swap) z₀ := by
…
```
Mentions: OAI.Nagata.Workers.W28.ComplexPlane

theorem OAI.Nagata.Workers.W28.homogeneous_normal_order_of_swapped_central_order line 140

Source documentation

The alternative tangential coordinate changes neither the homogeneous normal expression nor its variable frame and fiber weights.

theorem homogeneous_normal_order_of_swapped_central_order
    (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (d k : ℕ) (hhom : ∀ α ∈ I, (T α).IsHomogeneous (d-k*j α))
    (hbound : ∀ α ∈ I, k*j α ≤ d)
    (G : MvPolynomial (Fin 3) ℂ) (hG : G.IsHomogeneous k)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z₀ w₀ : ℂ)
    (hX : ∀ a, AnalyticAt ℂ (X a) z₀) (hc : X c z₀ ≠ 0)
    (hzero : ∀ᶠ z in 𝓝 z₀, MvPolynomial.eval (fun a => X a z) G = 0)
    (e : OpenPartialHomeomorph ComplexPlane ComplexPlane)
    (he : (e : ComplexPlane → ComplexPlane) = polynomialNormalCoordinates
      (Nagata.Workers.W17.affineSwap (Nagata.W27.directChartHom c G)))
    (hsource : (normalizedCurvePoint X c z₀).swap ∈ e.source) (m : ℕ)
…

Mentions: OAI.Nagata.Workers.W28.ComplexPlane, OAI.Nagata.Workers.W28.polynomialNormalCoordinates, OAI.Nagata.Workers.W17.affineSwap, OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.normalizedCurvePoint