Regularizing a nonzero analytic germ

The first nonzero homogeneous term of a convergent Taylor series is nonzero on some complex line. Extending that line to coordinates makes the germ regular in the last variable. This is the coordinate-change input required before Weierstrass preparation can be applied in Rückert's arguments.

Extending one nonzero direction to coordinates

noncomputable def LocalComplexGeometry.directionExtensionLinearEquiv {n : ℕ} (v : ComplexEuclidean (n + 1)) (j : Fin (n + 1)) (hvj : v j ≠ 0) : ClassicalComplexWPT.Ambient n ≃ₗ[ℂ] ComplexEuclidean (n + 1)

An explicit linear coordinate system whose distinguished axis is v.

The coordinate j, at which v is nonzero, is used as the pivot. The map is the elementary shear-and-rescaling (z,w) ↦ insert_j (w v_j) (z_i + w v_i).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LocalComplexGeometry.directionExtensionEquiv {n : ℕ} (v : ComplexEuclidean (n + 1)) (j : Fin (n + 1)) (hvj : v j ≠ 0) : ClassicalComplexWPT.Ambient n ≃L[ℂ] ComplexEuclidean (n + 1)

The preceding finite-dimensional linear equivalence is continuous.

Equations

• LocalComplexGeometry.directionExtensionEquiv v j hvj = (LocalComplexGeometry.directionExtensionLinearEquiv v j hvj).toContinuousLinearEquiv

@[simp]

theorem LocalComplexGeometry.directionExtensionEquiv_axis {n : ℕ} (v : ComplexEuclidean (n + 1)) (j : Fin (n + 1)) (hvj : v j ≠ 0) (w : ℂ) : (directionExtensionEquiv v j hvj) (0, w) = w • v

A nonzero germ has a nonzero homogeneous term on a line

theorem LocalComplexGeometry.HasFPowerSeriesAt.exists_nonzero_diagonal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {p : FormalMultilinearSeries ℂ E ℂ} (hp : HasFPowerSeriesAt f p 0) (hf : ¬f =ᶠ[nhds 0] fun (x : E) => 0) : ∃ (d : ℕ) (v : E), ((p d) fun (x : Fin d) => v) ≠ 0

If an analytic function is not the zero germ, one of the diagonal values of one of its homogeneous Taylor coefficients is nonzero.

This formulation is deliberate: multivariable formal multilinear series are only unique on their diagonals, and no unjustified symmetry assertion is used.

theorem LocalComplexGeometry.nonzero_of_diagonal_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (p : FormalMultilinearSeries ℂ E ℂ) (d : ℕ) (v : E) (hd : 0 < d) (h : ((p d) fun (x : Fin d) => v) ≠ 0) : v ≠ 0

A direction witnessing a nonzero homogeneous term is itself nonzero.

theorem LocalComplexGeometry.exists_nonzero_analytic_line {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (hf : AnalyticAt ℂ f 0) (hf_ne : ¬f =ᶠ[nhds 0] fun (x : E) => 0) (hf_zero : f 0 = 0) : ∃ (v : E) (p : FormalMultilinearSeries ℂ E ℂ) (d : ℕ), v ≠ 0 ∧ 0 < d ∧ HasFPowerSeriesAt f p 0 ∧ ((p d) fun (x : Fin d) => v) ≠ 0 ∧ ¬(fun (w : ℂ) => f (w • v)) =ᶠ[nhds 0] fun (x : ℂ) => 0

The restriction of a nonzero analytic germ to a suitable complex line is not the zero one-variable germ. The proof retains the witnessing nonzero Taylor coefficient.

Regularizing coordinate change

theorem LocalComplexGeometry.exists_regularizing_coordinateEquiv {n : ℕ} {f : ComplexEuclidean (n + 1) → ℂ} (hf : AnalyticAt ℂ f 0) (hf_ne : ¬f =ᶠ[nhds 0] fun (x : ComplexEuclidean (n + 1)) => 0) : ∃ (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (d : ℕ), ClassicalComplexWPT.ExactOrderInLastVariable (fun (x : ClassicalComplexWPT.Ambient n) => f (L ((wptAmbientEquiv n).symm x))) d

Every nonzero analytic germ on ℂⁿ⁺¹ becomes regular in the last variable after an invertible complex-linear coordinate change.

The returned natural number is the actual analytic order of the chosen line slice. Thus it is the least nonzero homogeneous order on that slice, not merely an arbitrary finite bound.

theorem LocalComplexGeometry.exists_regularizing_coordinateEquiv_pos {n : ℕ} {f : ComplexEuclidean (n + 1) → ℂ} (hf : AnalyticAt ℂ f 0) (hf_ne : ¬f =ᶠ[nhds 0] fun (x : ComplexEuclidean (n + 1)) => 0) (hf_zero : f 0 = 0) : ∃ (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (d : ℕ), 0 < d ∧ ClassicalComplexWPT.ExactOrderInLastVariable (fun (x : ClassicalComplexWPT.Ambient n) => f (L ((wptAmbientEquiv n).symm x))) d

If the germ vanishes at the origin, the regularized order is positive.