Documentation

LeanPool.LocalComplexGeometry.Nullstellensatz.OneVariable

The local analytic Nullstellensatz in one complex variable #

The proof uses the isolated-zero factorization of a nonzero one-variable analytic germ. A generator which is nonzero at the origin is a unit. If all generators vanish at the origin but one is a nonzero germ, its finite order of vanishing bounds a power of every germ vanishing at the origin. Finally, if all generators are zero germs, the common-zero hypothesis forces the target to be the zero germ.

The standard coordinate on ComplexEuclidean 1 #

source
def LocalComplexGeometry.oneCoordinateLinearEquiv :
ComplexEuclidean 1 ≃ₗ[ℂ] ℂ

Evaluation at the unique coordinate, as a complex-linear equivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LocalComplexGeometry.oneCoordinateEquiv :
    ComplexEuclidean 1 ≃L[ℂ] ℂ

    The continuous complex-linear identification ℂ¹ ≃ ℂ.

    Equations
    Instances For
      source
      @[simp]
      theorem LocalComplexGeometry.oneCoordinateEquiv_apply (x : ComplexEuclidean 1) :
      oneCoordinateEquiv x = x 0
      source
      @[simp]
      theorem LocalComplexGeometry.oneCoordinateEquiv_symm_apply (z : ℂ) :
      oneCoordinateEquiv.symm z = fun (x : Fin 1) => z

      A principal one-variable power certificate #

      source
      theorem LocalComplexGeometry.exists_power_eq_mul_of_analyticAt_oneVariable {f g : ComplexEuclidean 1 → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (hf_ne : ¬f =ᶠ[nhds 0] fun (x : ComplexEuclidean 1) => 0) :
      ∃ (N : ℕ), 0 < N ∧ ∃ (h : ComplexEuclidean 1 → ℂ), AnalyticAt ℂ h 0 ∧ (fun (x : ComplexEuclidean 1) => g x ^ N) =ᶠ[nhds 0] fun (x : ComplexEuclidean 1) => h x * f x

      If f is a nonzero one-variable analytic germ and both f and g vanish at the origin, then a positive power of g is an analytic multiple of f.

      The exponent produced by the proof is the order of vanishing of f.

      The finite-family Nullstellensatz #

      source
      theorem LocalComplexGeometry.localAnalyticNullstellensatz_oneVariable {s : ℕ} {f : Fin s → ComplexEuclidean 1 → ℂ} {g : ComplexEuclidean 1 → ℂ} (hf : ∀ (i : Fin s), AnalyticAt ℂ (f i) 0) (hg : AnalyticAt ℂ g 0) (hzero : ∀ᶠ (x : ComplexEuclidean 1) in nhds 0, (∀ (i : Fin s), f i x = 0) → g x = 0) :
      ∃ (N : ℕ), 0 < N ∧ ∃ (h : Fin s → ComplexEuclidean 1 → ℂ), (∀ (i : Fin s), AnalyticAt ℂ (h i) 0) ∧ (fun (x : ComplexEuclidean 1) => g x ^ N) =ᶠ[nhds 0] fun (x : ComplexEuclidean 1) => ∑ i : Fin s, h i x * f i x

      The audited finite-family local analytic Nullstellensatz in one complex variable. The hypothesis is the genuine eventual common-zero implication, and the conclusion is a positive-power certificate with analytic coefficients.