The algebraic uniqueness layer for Weierstrass preparation

The analytic preparation proof eventually reduces, at every nearby base point, to division in the weighted coefficient algebra ℓ¹(ℕ). This file records the precise uniqueness consequences of the division theorem, independently of the construction of the analytic coefficient maps.

The important application has two normal-form decompositions of the same coefficient sequence with respect to w^d + p:

• the quotient is the weighted coefficient sequence of the ratio of two units and the remainder is zero;
• the quotient is the constant sequence 1 and the remainder is the difference of the two prepared polynomials.

Since both remainders are supported in degrees below d, uniqueness of division identifies both the quotient and the remainder.

noncomputable def ClassicalComplexWPT.constantOneSeq : ↥(L1Coeff ℕ)

The coefficient sequence of the constant power series 1.

Equations

• ClassicalComplexWPT.constantOneSeq = lp.single 1 0 1

@[simp]

theorem ClassicalComplexWPT.constantOneSeq_apply (k : ℕ) : ↑constantOneSeq k = if k = 0 then 1 else 0

@[simp]

theorem ClassicalComplexWPT.convolution_constantOneSeq (q : ↥(L1Coeff ℕ)) : convolution constantOneSeq q = q

The constant sequence is the multiplicative identity for Cauchy convolution.

noncomputable def ClassicalComplexWPT.preparedTailSeq {n : ℕ} (r : NNReal) (d : ℕ) (a : Fin d → Base n → ℂ) (z : Base n) : ↥L1Sequence

The normalized weighted low-degree tail of a prepared polynomial. Its i-th coordinate is r^i / r^d * a_i(z); adding the shifted constant sequence gives the coefficients of r^{-d} P(z,rw).

Equations

• ClassicalComplexWPT.preparedTailSeq r d a z = ∑ i : Fin d, ((↑↑r ^ d)⁻¹ * ↑↑r ^ ↑i) • lp.single 1 (↑i) (a i z)

@[simp]

theorem ClassicalComplexWPT.preparedTailSeq_apply_fin {n d : ℕ} (r : NNReal) (a : Fin d → Base n → ℂ) (z : Base n) (i : Fin d) : ↑(preparedTailSeq r d a z) ↑i = (↑↑r ^ d)⁻¹ * ↑↑r ^ ↑i * a i z

@[simp]

theorem ClassicalComplexWPT.seqHighShift_preparedTailSeq {n d : ℕ} (r : NNReal) (a : Fin d → Base n → ℂ) (z : Base n) : seqHighShift d (preparedTailSeq r d a z) = 0

Prepared tails have no coefficients in degrees at least d.

theorem ClassicalComplexWPT.analyticAt_preparedTailSeq {n d : ℕ} (r : NNReal) (a : Fin d → Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : AnalyticAt ℂ (preparedTailSeq r d a) 0

The prepared tail varies analytically with the base point.

theorem ClassicalComplexWPT.eventually_norm_preparedTailSeq_lt_one {n d : ℕ} (r : NNReal) (a : Fin d → Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : ∀ᶠ (z : Base n) in nhds 0, ‖preparedTailSeq r d a z‖ < 1

Since all prepared coefficients vanish at the base origin, every fixed positive weighted tail is small on a sufficiently small base neighborhood.

theorem ClassicalComplexWPT.preparedTailSeq_eq_iff {n d : ℕ} {r : NNReal} (hr : 0 < r) (a a' : Fin d → Base n → ℂ) (z : Base n) : preparedTailSeq r d a z = preparedTailSeq r d a' z ↔ ∀ (i : Fin d), a i z = a' i z

Equality of normalized prepared tails recovers equality of every coefficient when the weight is positive.

theorem ClassicalComplexWPT.seqLowShift_constantOneSeq (d : ℕ) : seqLowShift d constantOneSeq = monomialSeq d

theorem ClassicalComplexWPT.evalL1PowerSeries_add_local (a b : ↥L1Sequence) (w : ℂ) : evalL1PowerSeries (a + b) w = evalL1PowerSeries a w + evalL1PowerSeries b w

theorem ClassicalComplexWPT.eval_preparedPolynomialSeq {n d : ℕ} (r : NNReal) (hr : 0 < r) (a : Fin d → Base n → ℂ) (z : Base n) {w : ℂ} (hw : ‖w‖ < 1) : evalL1PowerSeries (seqLowShift d constantOneSeq + preparedTailSeq r d a z) w = (↑↑r ^ d)⁻¹ * preparedPolynomial d a (z, ↑↑r * w)

Evaluation of the normalized prepared-polynomial coefficient sequence.

theorem ClassicalComplexWPT.eq_of_evalL1PowerSeries_eventuallyEq (a b : ↥L1Sequence) (h : (fun (w : ℂ) => evalL1PowerSeries a w) =ᶠ[nhds 0] fun (w : ℂ) => evalL1PowerSeries b w) : a = b

The analytic function on the unit disc represented by an ℓ¹ sequence determines every coefficient. The hypothesis is stated as germ equality, which is exactly what is available after shrinking the common analytic neighborhood in preparation uniqueness.

theorem ClassicalComplexWPT.seqDivision_factorizations_unique (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f q₁ r₁ q₂ r₂ : ↥(L1Coeff ℕ)) (hfac₁ : f = seqLowShift d q₁ + convolution q₁ p + r₁) (hr₁ : seqHighShift d r₁ = 0) (hfac₂ : f = seqLowShift d q₂ + convolution q₂ p + r₂) (hr₂ : seqHighShift d r₂ = 0) : q₁ = q₂ ∧ r₁ = r₂

Any two quotient/remainder decompositions for the same small normalized divisor agree. This is the form of seqDivision_existsUnique used by germ uniqueness.

theorem ClassicalComplexWPT.seqDivision_zero_remainder_unique (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f q q' r : ↥(L1Coeff ℕ)) (hfac : f = seqLowShift d q + convolution q p) (hfac' : f = seqLowShift d q' + convolution q' p + r) (hr : seqHighShift d r = 0) : q = q' ∧ r = 0

Specialized two-factorization principle used in preparation uniqueness: if one decomposition has zero remainder and another has a low-degree remainder, then the quotients agree and that remainder vanishes.

theorem ClassicalComplexWPT.seqPreparedPolynomial_unique (d : ℕ) (p p' v : ↥(L1Coeff ℕ)) (hp' : ‖p'‖ < 1) (hpLow : seqHighShift d p = 0) (hp'Low : seqHighShift d p' = 0) (hfactor : seqLowShift d constantOneSeq + p = seqLowShift d v + convolution v p') : p = p' ∧ v = constantOneSeq

Abstract uniqueness of a prepared polynomial. Here p and p' are the low-degree tails of two monic degree-d polynomials, while v is the coefficient sequence of the ratio of their analytic units. The displayed identity says (w^d + p) = v * (w^d + p') in weighted coefficients.

This theorem is deliberately independent of how the coefficient sequences were extracted from analytic germs.

theorem ClassicalComplexWPT.seqPreparedPolynomial_unique_of_eventually_eval (d : ℕ) (p p' v : ↥(L1Coeff ℕ)) (hp' : ‖p'‖ < 1) (hpLow : seqHighShift d p = 0) (hp'Low : seqHighShift d p' = 0) (heval : (fun (w : ℂ) => evalL1PowerSeries (seqLowShift d constantOneSeq + p) w) =ᶠ[nhds 0] fun (w : ℂ) => evalL1PowerSeries (seqLowShift d v + convolution v p') w) : p = p' ∧ v = constantOneSeq

Evaluation-level form of seqPreparedPolynomial_unique. This avoids any need for a multivariable uniqueness theorem: after fixing the base point, the ordinary one-variable uniqueness theorem identifies the two ℓ¹ coefficient sequences.

theorem ClassicalComplexWPT.isWeierstrassPreparation_unique {n d : ℕ} {f : Ambient n → ℂ} {a a' : Fin d → Base n → ℂ} {u u' : Ambient n → ℂ} (h : IsWeierstrassPreparation f d a u) (h' : IsWeierstrassPreparation f d a' u') : (∀ (i : Fin d), a i =ᶠ[nhds 0] a' i) ∧ u =ᶠ[nhds 0] u'

Full germ uniqueness of Weierstrass preparation witnesses.