The radius of a power series

The radius of a power series f = ∑ aₙ Xⁿ over a normed ring is the supremum, in ℝ≥0∞, of the nonnegative real radii r at which f is restricted, that is, at which ‖aₙ‖ rⁿ → 0. It is an invariant of the coefficient norms alone: it does not refer to points at which f might be evaluated, so it does not depend on a choice of extension field, and an isometric change of coefficients preserves it. Polynomials, including zero, have radius ∞.

The series is restricted at every radius of absolute value strictly below its radius and at no radius strictly above it; at the radius itself the radius alone decides nothing. Restrictedness at r may be replaced by boundedness of the weighted coefficient norms ‖aₙ‖ rⁿ, which makes the radius agree with Mathlib's FormalMultilinearSeries.radius of any formal multilinear series with the same coefficient norms. Through this comparison the Cauchy–Hadamard formula 1 / radius f = limsup ‖aₙ‖ ^ (1 / n) follows from FormalMultilinearSeries.radius_inv_eq_limsup, and Mathlib's ratio tests for FormalMultilinearSeries.ofScalars apply to series over a nontrivially normed field.

Main definitions

• PowerSeries.radius f: the supremum of the radii r ≥ 0 at which f is restricted.

Main results

• PowerSeries.isRestricted_of_lt_radius and PowerSeries.not_isRestricted_of_radius_lt: f is restricted at every r with |r| < radius f and at no r with radius f < |r|.
• PowerSeries.le_radius_of_bound: bounded weighted coefficient norms at r give r ≤ radius f.
• PowerSeries.radius_eq_top_iff: the radius is infinite exactly for entire series; in particular PowerSeries.radius_coe: polynomials have infinite radius.
• PowerSeries.radius_pos_iff: the radius is positive exactly when the series is restricted at some positive radius.
• PowerSeries.radius_eq_radius_of_norm_eq and PowerSeries.radius_eq_radius_ofScalars: the radius is the radius of any formal multilinear series with the same coefficient norms.
• PowerSeries.radius_eq_liminf and PowerSeries.radius_inv_eq_limsup: the Cauchy–Hadamard formula.
• PowerSeries.radius_map: isometric coefficient maps preserve the radius.
• PowerSeries.radius_mk_pow: over a ring with multiplicative norm, the geometric series ∑ aⁿ Xⁿ has radius ‖a‖⁻¹.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §1.
• M. Lazard, Les zéros d'une fonction analytique d'une variable sur un corps valué complet, Publications Mathématiques de l'IHÉS 14 (1962), §1.

noncomputable def PowerSeries.radius {R : Type u_1} [NormedRing R] (f : PowerSeries R) : ENNReal

The radius of a power series f = ∑ aₙ Xⁿ: the supremum of the radii r ≥ 0 at which f is restricted, that is, at which ‖aₙ‖ rⁿ → 0.

theorem PowerSeries.radius_def {R : Type u_1} [NormedRing R] (f : PowerSeries R) : f.radius = ⨆ (r : NNReal), ⨆ (_ : IsRestricted (↑r) f), ↑r

The radius as the supremum of the radii of restrictedness.

theorem PowerSeries.le_radius_of_isRestricted {R : Type u_1} [NormedRing R] {f : PowerSeries R} {r : ℝ} (hf : IsRestricted r f) : ‖r‖ₑ ≤ f.radius

A series restricted at r has radius at least |r|.

theorem PowerSeries.isRestricted_of_lt_radius {R : Type u_1} [NormedRing R] {f : PowerSeries R} {r : ℝ} (h : ‖r‖ₑ < f.radius) : IsRestricted r f

A series is restricted at every radius of absolute value strictly below its radius.

theorem PowerSeries.not_isRestricted_of_radius_lt {R : Type u_1} [NormedRing R] {f : PowerSeries R} {r : ℝ} (h : f.radius < ‖r‖ₑ) : ¬IsRestricted r f

A series is not restricted at any radius of absolute value strictly above its radius.

theorem PowerSeries.le_radius_of_bound {R : Type u_1} [NormedRing R] {f : PowerSeries R} (C : ℝ) {r : NNReal} (h : ∀ (n : ℕ), ‖(coeff n) f‖ * ↑r ^ n ≤ C) : ↑r ≤ f.radius

If the weighted coefficient norms ‖aₙ‖ rⁿ are bounded, the radius is at least r.

@[simp]

theorem PowerSeries.radius_eq_top_iff {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f.radius = ⊤ ↔ f.IsEntire

The radius is infinite exactly when the series is entire.

@[simp]

theorem PowerSeries.radius_coe {R : Type u_1} [NormedRing R] (p : Polynomial R) : (↑p).radius = ⊤

Polynomials have infinite radius.

@[simp]

theorem PowerSeries.radius_zero {R : Type u_1} [NormedRing R] : radius 0 = ⊤

The zero series has infinite radius.

theorem PowerSeries.radius_pos_iff {R : Type u_1} [NormedRing R] {f : PowerSeries R} : 0 < f.radius ↔ ∃ (r : ℝ), 0 < r ∧ IsRestricted r f

The radius is positive exactly when the series is restricted at some positive radius.

theorem PowerSeries.radius_eq_radius_of_norm_eq {R : Type u_1} [NormedRing R] {f : PowerSeries R} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (h : ∀ (n : ℕ), ‖p n‖ = ‖(coeff n) f‖) : f.radius = p.radius

Comparison with formal multilinear series. The radius of f is the radius of any formal multilinear series whose terms have the norms of the coefficients of f.

theorem PowerSeries.radius_le_radius_of_norm_coeff_le {R : Type u_1} {S : Type u_2} [NormedRing R] [NormedRing S] {f : PowerSeries R} {g : PowerSeries S} (h : ∀ (n : ℕ), ‖(coeff n) g‖ ≤ ‖(coeff n) f‖) : f.radius ≤ g.radius

Comparison of radii. If the coefficients of g are no larger in norm than those of f, the radius of g is at least that of f.

theorem PowerSeries.radius_map {R : Type u_1} {S : Type u_2} [NormedRing R] [NormedRing S] {f : PowerSeries R} (φ : R →+* S) (hφ : ∀ (x : R), ‖φ x‖ = ‖x‖) : ((map φ) f).radius = f.radius

Coefficient maps preserving norms preserve the radius.

theorem PowerSeries.min_radius_le_radius_add {R : Type u_1} [NormedRing R] (f g : PowerSeries R) : min f.radius g.radius ≤ (f + g).radius

The radius of a sum is at least the smaller of the two radii.

theorem PowerSeries.min_radius_le_radius_mul {R : Type u_1} [NormedRing R] (f g : PowerSeries R) : min f.radius g.radius ≤ (f * g).radius

The radius of a product is at least the smaller of the two radii.

theorem PowerSeries.radius_eq_liminf {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f.radius = Filter.liminf (fun (n : ℕ) => 1 / ↑(‖(coeff n) f‖₊ ^ (1 / ↑n))) Filter.atTop

Cauchy–Hadamard formula, liminf form: the radius of ∑ aₙ Xⁿ is liminf 1 / ‖aₙ‖ ^ (1 / n).

theorem PowerSeries.radius_inv_eq_limsup {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f.radius⁻¹ = Filter.limsup (fun (n : ℕ) => ↑(‖(coeff n) f‖₊ ^ (1 / ↑n))) Filter.atTop

Cauchy–Hadamard formula: the inverse of the radius of ∑ aₙ Xⁿ is limsup ‖aₙ‖ ^ (1 / n).

theorem PowerSeries.radius_mk_pow {R : Type u_1} [NormedRing R] [NormMulClass R] (a : R) : (mk fun (n : ℕ) => a ^ n).radius = (↑‖a‖₊)⁻¹

Over a ring with multiplicative norm, the geometric series ∑ aⁿ Xⁿ has radius ‖a‖⁻¹. For a ≠ 0 it is restricted at every smaller radius but not at ‖a‖⁻¹ itself; for a = 0 it is the constant 1 and the radius is ∞.

theorem PowerSeries.radius_eq_radius_ofScalars {K : Type u_1} [NontriviallyNormedField K] (E : Type u_2) [NormedRing E] [NormOneClass E] [NormedAlgebra K E] (f : PowerSeries K) : f.radius = (FormalMultilinearSeries.ofScalars E fun (n : ℕ) => (coeff n) f).radius

Over a nontrivially normed field K, the radius of f is the radius of the scalar formal multilinear series FormalMultilinearSeries.ofScalars E (coeff · f) in any normed K-algebra E with ‖1‖ = 1.