Strassmann's theorem

Let K be a complete ultrametric normed field and f = ∑ aₙ Xⁿ a nonzero power series over K restricted at a radius c > 0, so that ‖aₙ‖ cⁿ → 0. Let s be the largest index at which the weighted coefficient norm ‖aₙ‖ cⁿ attains its maximum, so that f is distinguished of degree s at c (TauCeti.PowerSeries.IsDistinguished). Strassmann's theorem says that f has at most s distinct zeros in the closed disc of radius c, and this holds in every complete normed field L containing K isometrically.

Weierstrass preparation writes f = e * ω with ω a monic polynomial of degree s and e a unit of the ring of series restricted at c. Evaluation at a point x with ‖x‖ ≤ c is a ring homomorphism on that ring, so it sends e to a unit, and the zeros of f in the disc are roots of ω. The field L is automatically ultrametric, since K is and L is a normed K-algebra.

At points of K, counting zeros with their multiplicities, the orders of the good zeros of f in the closed disc add up to at most s, since they are root multiplicities of ω. Every root of a polynomial P with f = u * P, u a unit of the ring of series restricted at c and P of degree at most s, lies in the closed disc, so over an algebraically closed K the bound is an equality: the zeros of f in the closed disc, counted with multiplicity, number exactly s.

As a consequence, a nonzero series restricted at c has only finitely many zeros in the closed disc of radius c, so a series restricted at c that vanishes on an infinite subset of that disc is zero. The bound is sharp: X ^ p - X over ℚ_p is distinguished of degree p at the unit radius and vanishes at the p Teichmüller representatives in ℤ_p.

The identity principle extends to series with coefficients in a normed space E over K that carries a jointly injective family of continuous linear maps φⱼ : E → Lⱼ into complete normed field extensions of K: each φⱼ turns such a series into a restricted series over Lⱼ.

Main results

• TauCeti.PowerSeries.IsDistinguished.encard_setOf_evalAt_eq_zero_le: Strassmann's theorem.
• TauCeti.PowerSeries.IsDistinguished.sum_le_of_isGoodZero: Strassmann's theorem with multiplicities.
• TauCeti.PowerSeries.IsDistinguished.norm_le_of_mem_roots_of_isUnit_mul: the prepared polynomial has its roots in the closed disc.
• TauCeti.PowerSeries.IsDistinguished.exists_card_eq_isGoodZero: over an algebraically closed field, a series distinguished of degree s at c > 0 has exactly s zeros in the closed disc, counted with multiplicity.
• PowerSeries.IsRestricted.finite_setOf_norm_le_and_evalAt_eq_zero: a nonzero restricted series has finitely many zeros in the closed disc.
• PowerSeries.IsRestricted.eq_zero_of_infinite_of_evalAt_eq_zero: the identity principle for restricted series.
• TauCeti.PowerSeries.eq_zero_of_hasSum_pow_smul: the identity principle for series with coefficients in a normed space with a jointly injective family of functionals into complete field extensions.

References

• R. Strassmann, Über den Wertevorrat von Potenzreihen im Gebiet der p-adischen Zahlen, J. Reine Angew. Math. 159 (1928), 13–28.
• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.2, Theorem 1 (Weierstrass preparation), from which the bound is deduced.

theorem TauCeti.PowerSeries.IsDistinguished.norm_le_of_mem_roots_of_isUnit_mul {K : Type u_1} [NormedField K] [IsUltrametricDist K] {c : ℝ} {s : ℕ} {f : PowerSeries K} (hf : IsDistinguished c s f) (hc : 0 < c) {u : ↥(PowerSeries.IsRestricted.subring c)} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ s) (hmul : ↑u * ↑P = f) {α : K} (hα : α ∈ P.roots) : ‖α‖ ≤ c

The prepared polynomial has its roots in the closed disc. If f is distinguished of degree s at c > 0 and f = u * P with u a unit of the ring of series restricted at c and P a polynomial of degree at most s, then every root of P has norm at most c.

theorem TauCeti.PowerSeries.IsDistinguished.encard_setOf_evalAt_eq_zero_le {K : Type u_1} {L : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [NormedField L] [NormedAlgebra K L] [CompleteSpace L] {c : ℝ} {s : ℕ} {f : PowerSeries K} (hf : IsDistinguished c s f) (hc : 0 < c) (hfr : PowerSeries.IsRestricted c f) : {x : L | ‖x‖ ≤ c ∧ f.evalAt x = 0}.encard ≤ ↑s

Strassmann's theorem. Let f be a power series over a complete ultrametric normed field K, restricted at a radius c > 0 and distinguished of degree s there, that is, s is the largest index at which the weighted coefficient norm ‖aₙ‖ cⁿ attains the Gauss norm. Then f has at most s zeros of norm at most c in any complete normed field extension L of K.

theorem TauCeti.PowerSeries.IsDistinguished.sum_le_of_isGoodZero {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} {s : ℕ} {f : PowerSeries K} (hfd : IsDistinguished c s f) (hc : 0 < c) (hfr : PowerSeries.IsRestricted c f) {S : Finset K} {h : K → ℕ} (hS : ∀ a ∈ S, ‖a‖ ≤ c ∧ f.IsGoodZero a (h a)) : ∑ a ∈ S, h a ≤ s

Strassmann's theorem with multiplicities. Let f be restricted at c > 0 and distinguished of degree s there. If f has a good zero of order h a at each point a of a finite set S in the closed disc of radius c, then ∑_{a ∈ S} h a ≤ s.

theorem TauCeti.PowerSeries.IsDistinguished.exists_card_eq_isGoodZero {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} {s : ℕ} {f : PowerSeries K} [IsAlgClosed K] [DecidableEq K] (hfd : IsDistinguished c s f) (hc : 0 < c) (hfr : PowerSeries.IsRestricted c f) : ∃ (Z : Multiset K), Z.card = s ∧ (∀ a ∈ Z, ‖a‖ ≤ c) ∧ ∀ (a : K), ‖a‖ ≤ c → f.IsGoodZero a (Multiset.count a Z)

Zeros in a closed disc, with multiplicity. Over an algebraically closed field, the zeros of a series f restricted at c > 0 and distinguished of degree s there, in the closed disc of radius c and counted with multiplicity, form a multiset Z with exactly s elements: f has a good zero of order Z.count a at every a of norm at most c.

theorem PowerSeries.IsRestricted.finite_setOf_norm_le_and_evalAt_eq_zero {K : Type u_1} {L : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [NormedField L] [NormedAlgebra K L] [CompleteSpace L] {c : ℝ} {f : PowerSeries K} (hfr : IsRestricted c f) (hc : 0 < c) (hf0 : f ≠ 0) : {x : L | ‖x‖ ≤ c ∧ f.evalAt x = 0}.Finite

A nonzero power series over a complete ultrametric normed field, restricted at a radius c > 0, has only finitely many zeros of norm at most c in any complete normed field extension.

theorem PowerSeries.IsRestricted.eq_zero_of_infinite_of_evalAt_eq_zero {K : Type u_1} {L : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [NormedField L] [NormedAlgebra K L] [CompleteSpace L] {c : ℝ} {f : PowerSeries K} (hfr : IsRestricted c f) (hc : 0 < c) {S : Set L} (hS : S.Infinite) (hSc : ∀ x ∈ S, ‖x‖ ≤ c) (hfS : ∀ x ∈ S, f.evalAt x = 0) : f = 0

Identity principle for restricted series. A power series over a complete ultrametric normed field, restricted at a radius c > 0, that vanishes on an infinite set of points of norm at most c in a complete normed field extension is zero.

theorem TauCeti.PowerSeries.eq_zero_of_hasSum_pow_smul {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [NormedAddCommGroup E] [NormedSpace K E] {ι : Type u_3} {L : ι → Type u_4} [(j : ι) → NormedField (L j)] [(j : ι) → NormedAlgebra K (L j)] [∀ (j : ι), CompleteSpace (L j)] (φ : (j : ι) → E →L[K] L j) (hφ : ∀ (e : E), (∀ (j : ι), (φ j) e = 0) → e = 0) {r : ℝ} {β : ℕ → E} (hβ : Filter.Tendsto (fun (k : ℕ) => ‖β k‖ * r ^ k) Filter.atTop (nhds 0)) {S : Set K} (hS : S.Infinite) (hSr : ∀ x ∈ S, ‖x‖ ≤ r) (h : ∀ x ∈ S, HasSum (fun (k : ℕ) => x ^ k • β k) 0) : β = 0

Identity principle for module-valued series. Let E be a normed space over an ultrametric nontrivially normed field K, with a jointly injective family of continuous linear maps φⱼ : E → Lⱼ into complete normed field extensions of K. A sequence β in E with ‖β k‖ rᵏ → 0, whose series ∑ₖ xᵏ • β k sums to zero at every point of an infinite subset of the disc of radius r, is zero.