Power series on an open disc

A power series f = ∑ aₙ Xⁿ over a normed ring lies on the open disc of radius R₀ when it is restricted at every radius 0 < r < R₀, that is, ‖aₙ‖ rⁿ → 0 for each such r. No condition is imposed on the boundary circle ‖x‖ = R₀: over a complete ultrametric ring such a series can be summed at every x with ‖x‖ < R₀, being restricted at a radius strictly between ‖x‖ and R₀. These series form the coefficient algebra of analytic functions on an open disc. They sit between the series restricted at the radius R₀ and the entire series: a series restricted at R₀ lies on the open disc of radius R₀ (PowerSeries.IsRestricted.onOpenDisc), and a series is entire exactly when it lies on every open disc (PowerSeries.isEntire_iff_forall_onOpenDisc). Mathlib's FormalMultilinearSeries.radius measures the same growth for series of multilinear maps over a nontrivially normed field; here the coefficients lie in an arbitrary normed ring, which may have nilpotents, and the series are native power series carrying the restricted-series API.

The condition can equivalently be tested along any family of radii below R₀ tending to R₀ (PowerSeries.onOpenDisc_iff_of_tendsto), for instance along a sequence, and it amounts to bounded weighted coefficient norms at every smaller radius (PowerSeries.onOpenDisc_iff_forall_hasGaussNorm). In particular, a series with bounded coefficients lies on the open unit disc (PowerSeries.onOpenDisc_of_bddAbove_norm_coeff); this is the inclusion of bounded-coefficient series into the open unit-disc algebra used in Iwasawa theory.

No ultrametric hypothesis is needed for the algebraic structure: products and Hasse derivatives only lose an arbitrarily small amount of radius, which the open condition absorbs. Thus over any normed ring the series on the open disc of radius R₀ form a subring PowerSeries.OnOpenDisc.subring R R₀, stable under Hasse derivatives and bounded coefficient maps.

The geometric series ∑ aⁿ Xⁿ lies on the open disc of radius ‖a‖⁻¹ (PowerSeries.onOpenDisc_mk_pow), but for a ≠ 0 and a multiplicative norm it is not restricted at that radius (TauCeti.PowerSeries.not_isRestricted_mk_pow). Similarly, over a nontrivial normed ring, ∑ Xⁿ lies on the open unit disc without being restricted at the radius 1 (PowerSeries.onOpenDisc_mk_one, TauCeti.PowerSeries.not_isRestricted_mk_one). Over a normed field of characteristic zero, the logarithm series log (1 + X) = ∑ (-1) ^ (n + 1) Xⁿ / n lies on the open unit disc (PowerSeries.onOpenDisc_log).

Main definitions

• PowerSeries.OnOpenDisc: f is restricted at every radius 0 < r < R₀.
• PowerSeries.OnOpenDisc.subring: the subring of series on the open disc of radius R₀.

Main results

• PowerSeries.OnOpenDisc.summable_norm_coeff_mul_pow: the weighted coefficient norms ‖coeff n f‖ * t ^ n are summable for |t| < R₀.
• PowerSeries.OnOpenDisc.summable_norm_coeff_mul_pow' and PowerSeries.OnOpenDisc.summable_coeff_mul_pow: absolute summability at points inside the disc, and summability when the coefficient ring is complete.
• PowerSeries.OnOpenDisc.isRestricted: a series on the open disc of radius R₀ is restricted at every radius r with |r| < R₀; PowerSeries.OnOpenDisc.isRestricted_max is the form for the larger of two radii below R₀, one of them nonnegative.
• PowerSeries.onOpenDisc_iff_of_tendsto: the condition can be tested along radii tending to R₀ from below.
• PowerSeries.onOpenDisc_iff_forall_hasGaussNorm: the condition amounts to bounded weighted coefficient norms at every smaller radius.
• PowerSeries.HasGaussNorm.onOpenDisc: bounded weighted coefficients at R₀ give a series on the open disc of radius R₀; PowerSeries.onOpenDisc_of_bddAbove_norm_coeff is the case R₀ = 1.
• PowerSeries.IsRestricted.onOpenDisc and PowerSeries.isEntire_iff_forall_onOpenDisc: the comparisons with restricted and entire series.
• PowerSeries.OnOpenDisc.add, PowerSeries.OnOpenDisc.mul, PowerSeries.onOpenDisc_coe and their companions: these series form a subring containing the polynomials.
• PowerSeries.OnOpenDisc.hasseDeriv, PowerSeries.OnOpenDisc.derivative and PowerSeries.OnOpenDisc.map: the condition is preserved by Hasse derivatives and bounded coefficient maps.
• PowerSeries.OnOpenDisc.rescale: if f(X) lies on the open disc of radius ‖a‖ * R₀, then f(aX) lies on the open disc of radius R₀.
• PowerSeries.onOpenDisc_log: over a normed field of characteristic zero, log (1 + X) lies on the open unit disc.

References

• P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), 13–59.

def PowerSeries.OnOpenDisc {R : Type u_1} [NormedRing R] (R₀ : ℝ) (f : PowerSeries R) : Prop

A power series f = ∑ aₙ Xⁿ lies on the open disc of radius R₀ when it is restricted at every radius 0 < r < R₀, that is, ‖aₙ‖ rⁿ → 0 for each such r.

theorem PowerSeries.onOpenDisc_iff {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} : OnOpenDisc R₀ f ↔ ∀ (r : ℝ), 0 < r → r < R₀ → IsRestricted r f

A series lies on the open disc of radius R₀ exactly when it is restricted at every radius 0 < r < R₀.

theorem PowerSeries.OnOpenDisc.isRestricted {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) {r : ℝ} (hr : |r| < R₀) : IsRestricted r f

A series on the open disc of radius R₀ is restricted at every radius r with |r| < R₀.

theorem PowerSeries.OnOpenDisc.isRestricted_max {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) {s t : ℝ} (hs : 0 ≤ s) (hsR : s < R₀) (htR : t < R₀) : IsRestricted (max s t) f

A series on the open disc of radius R₀ is restricted at the larger of a nonnegative radius s < R₀ and a radius t < R₀.

theorem PowerSeries.OnOpenDisc.summable_norm_coeff_mul_pow {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) {t : ℝ} (ht : |t| < R₀) : Summable fun (n : ℕ) => ‖(coeff n) f‖ * t ^ n

Inside its open disc, the weighted coefficient norms of a power series are summable. No completeness or ultrametric hypothesis is needed.

theorem PowerSeries.OnOpenDisc.summable_norm_coeff_mul_pow' {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) {t : R} (ht : ‖t‖ < R₀) : Summable fun (n : ℕ) => ‖(coeff n) f * t ^ n‖

A series on an open disc is absolutely summable at every point inside the disc.

theorem PowerSeries.OnOpenDisc.summable_coeff_mul_pow {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} [CompleteSpace R] (hf : OnOpenDisc R₀ f) {t : R} (ht : ‖t‖ < R₀) : Summable fun (n : ℕ) => (coeff n) f * t ^ n

Over a complete normed ring, a series on an open disc is summable at every point inside the disc.

theorem PowerSeries.onOpenDisc_of_nonpos {R : Type u_1} [NormedRing R] {R₀ : ℝ} (h : R₀ ≤ 0) (f : PowerSeries R) : OnOpenDisc R₀ f

For a nonpositive radius R₀ the open disc is empty, and every series lies on it.

theorem PowerSeries.OnOpenDisc.mono {R : Type u_1} [NormedRing R] {R₀ R₁ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) (h : R₁ ≤ R₀) : OnOpenDisc R₁ f

A series on an open disc lies on every smaller open disc.

theorem PowerSeries.onOpenDisc_iff_of_tendsto {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} {ι : Type u_2} {l : Filter ι} [l.NeBot] {ρ : ι → ℝ} (hρ : ∀ (i : ι), |ρ i| < R₀) (hlim : Filter.Tendsto ρ l (nhds R₀)) : OnOpenDisc R₀ f ↔ ∀ (i : ι), IsRestricted (ρ i) f

The condition of lying on the open disc of radius R₀ can be tested along any family of radii ρ i with |ρ i| < R₀ tending to R₀, for instance along a sequence. In particular it does not depend on the choice of such a family.

theorem PowerSeries.IsRestricted.onOpenDisc {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : IsRestricted R₀ f) : OnOpenDisc R₀ f

A series restricted at the radius R₀ lies on the open disc of radius R₀.

theorem PowerSeries.HasGaussNorm.onOpenDisc {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : HasGaussNorm norm R₀ f) : OnOpenDisc R₀ f

A series whose weighted coefficient norms ‖aₙ‖ R₀ⁿ are bounded lies on the open disc of radius R₀.

theorem PowerSeries.onOpenDisc_iff_forall_hasGaussNorm {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} : OnOpenDisc R₀ f ↔ ∀ (r : ℝ), 0 < r → r < R₀ → HasGaussNorm norm r f

A series lies on the open disc of radius R₀ exactly when its weighted coefficient norms are bounded at every radius 0 < r < R₀.

theorem PowerSeries.onOpenDisc_of_bddAbove_norm_coeff {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : BddAbove (Set.range fun (n : ℕ) => ‖(coeff n) f‖)) : OnOpenDisc 1 f

A series with bounded coefficients lies on the open unit disc.

theorem PowerSeries.IsEntire.onOpenDisc {R : Type u_1} [NormedRing R] {f : PowerSeries R} (hf : f.IsEntire) (R₀ : ℝ) : OnOpenDisc R₀ f

An entire series lies on every open disc.

theorem PowerSeries.isEntire_iff_forall_onOpenDisc {R : Type u_1} [NormedRing R] {f : PowerSeries R} : f.IsEntire ↔ ∀ (R₀ : ℝ), OnOpenDisc R₀ f

A series is entire exactly when it lies on every open disc.

@[simp]

theorem PowerSeries.onOpenDisc_zero {R : Type u_1} [NormedRing R] {R₀ : ℝ} : OnOpenDisc R₀ 0

The zero series lies on every open disc.

@[simp]

theorem PowerSeries.onOpenDisc_one {R : Type u_1} [NormedRing R] {R₀ : ℝ} : OnOpenDisc R₀ 1

The constant series 1 lies on every open disc.

@[simp]

theorem PowerSeries.onOpenDisc_C {R : Type u_1} [NormedRing R] {R₀ : ℝ} (a : R) : OnOpenDisc R₀ (C a)

Constant series lie on every open disc.

@[simp]

theorem PowerSeries.onOpenDisc_monomial {R : Type u_1} [NormedRing R] {R₀ : ℝ} (n : ℕ) (a : R) : OnOpenDisc R₀ ((monomial n) a)

Monomials lie on every open disc.

@[simp]

theorem PowerSeries.onOpenDisc_X {R : Type u_1} [NormedRing R] {R₀ : ℝ} : OnOpenDisc R₀ X

The variable X lies on every open disc.

@[simp]

theorem PowerSeries.onOpenDisc_coe {R : Type u_1} [NormedRing R] {R₀ : ℝ} (p : Polynomial R) : OnOpenDisc R₀ ↑p

Every polynomial lies on every open disc.

theorem PowerSeries.OnOpenDisc.add {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f g : PowerSeries R} (hf : OnOpenDisc R₀ f) (hg : OnOpenDisc R₀ g) : OnOpenDisc R₀ (f + g)

A sum of series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.neg {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) : OnOpenDisc R₀ (-f)

The negative of a series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.sub {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f g : PowerSeries R} (hf : OnOpenDisc R₀ f) (hg : OnOpenDisc R₀ g) : OnOpenDisc R₀ (f - g)

A difference of series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.smul {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (a : R) (hf : OnOpenDisc R₀ f) : OnOpenDisc R₀ (a • f)

A scalar multiple a • f of a series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.sum {R : Type u_1} [NormedRing R] {R₀ : ℝ} {ι : Type u_2} {s : Finset ι} {f : ι → PowerSeries R} (hf : ∀ i ∈ s, OnOpenDisc R₀ (f i)) : OnOpenDisc R₀ (∑ i ∈ s, f i)

A finite sum of series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.mul {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f g : PowerSeries R} (hf : OnOpenDisc R₀ f) (hg : OnOpenDisc R₀ g) : OnOpenDisc R₀ (f * g)

A product of series on an open disc lies on that disc. Over a general normed ring, the product of two series restricted at a radius s is only restricted at the radii below s; the open condition provides such an s between r and R₀.

theorem PowerSeries.OnOpenDisc.pow {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) (n : ℕ) : OnOpenDisc R₀ (f ^ n)

A power of a series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.hasseDeriv {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) (k : ℕ) : OnOpenDisc R₀ ((PowerSeries.hasseDeriv k) f)

Hasse derivatives of a series on an open disc lie on that disc.

theorem PowerSeries.OnOpenDisc.map {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} {S : Type u_2} [NormedRing S] (hf : OnOpenDisc R₀ f) (φ : R →+* S) {C : ℝ} (hφ : ∀ (x : R), ‖φ x‖ ≤ C * ‖x‖) : OnOpenDisc R₀ ((PowerSeries.map φ) f)

A bounded ring homomorphism φ, ‖φ x‖ ≤ C ‖x‖, maps series on an open disc to series on that disc coefficientwise.

theorem PowerSeries.onOpenDisc_mk_pow {R : Type u_1} [NormedRing R] (a : R) : OnOpenDisc ‖a‖⁻¹ (mk fun (n : ℕ) => a ^ n)

The geometric series ∑ aⁿ Xⁿ lies on the open disc of radius ‖a‖⁻¹: at a radius r < ‖a‖⁻¹, its weighted coefficient norms are bounded by (‖a‖ r)ⁿ from n = 1 on.

theorem PowerSeries.onOpenDisc_mk_one {R : Type u_1} [NormedRing R] : OnOpenDisc 1 (mk 1)

The series ∑ Xⁿ lies on the open unit disc, its coefficients being bounded.

noncomputable def PowerSeries.OnOpenDisc.subring (R : Type u_1) [NormedRing R] (R₀ : ℝ) : Subring (PowerSeries R)

The power series on the open disc of radius R₀ form a subring.

@[simp]

theorem PowerSeries.OnOpenDisc.mem_subring {R : Type u_1} [NormedRing R] {R₀ : ℝ} {f : PowerSeries R} : f ∈ OnOpenDisc.subring R R₀ ↔ OnOpenDisc R₀ f

Membership in the subring of series on the open disc of radius R₀ is lying on that disc.

noncomputable def PowerSeries.OnOpenDisc.polynomialHom {R : Type u_1} [NormedRing R] {R₀ : ℝ} : Polynomial R →+* ↥(OnOpenDisc.subring R R₀)

The inclusion of polynomials into series on the open disc.

@[simp]

theorem PowerSeries.OnOpenDisc.coe_polynomialHom {R : Type u_1} [NormedRing R] {R₀ : ℝ} (p : Polynomial R) : ↑(polynomialHom p) = ↑p

Polynomial inclusion has the usual underlying formal power series.

theorem PowerSeries.OnOpenDisc.subring_antitone (R : Type u_1) [NormedRing R] : Antitone (OnOpenDisc.subring R)

The subring of series on the open disc of radius R₀ shrinks as R₀ grows.

theorem PowerSeries.IsEntire.subring_le_onOpenDiscSubring {R : Type u_1} [NormedRing R] (R₀ : ℝ) : IsEntire.subring R ≤ OnOpenDisc.subring R R₀

Entire series lie in the subring of series on every open disc.

theorem PowerSeries.IsRestricted.subring_le_onOpenDiscSubring {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (R₀ : ℝ) : subring R₀ ≤ OnOpenDisc.subring R R₀

Over an ultrametric ring, the subring of series restricted at R₀ lies in the subring of series on the open disc of radius R₀.

theorem PowerSeries.OnOpenDisc.derivative {R : Type u_1} [NormedCommRing R] {R₀ : ℝ} {f : PowerSeries R} (hf : OnOpenDisc R₀ f) : OnOpenDisc R₀ (PowerSeries.derivative f)

The derivative of a series on an open disc lies on that disc.

theorem PowerSeries.OnOpenDisc.rescale {R : Type u_1} [NormedCommRing R] {R₀ : ℝ} {f : PowerSeries R} {a : R} (hf : OnOpenDisc (‖a‖ * R₀) f) : OnOpenDisc R₀ ((PowerSeries.rescale a) f)

Rescaling changes the radius of the disc. If f(X) lies on the open disc of radius ‖a‖ * R₀, then f(aX) lies on the open disc of radius R₀. For a = 0 the series f(0 · X) is the constant f(0), which lies on every open disc.

theorem PowerSeries.norm_coeff_log_le {K : Type u_1} [NormedField K] [CharZero K] (n : ℕ) : ‖(coeff n) (log K)‖ ≤ ‖(↑n)⁻¹‖

The coefficients (-1) ^ (n + 1) / n of log (1 + X) are dominated by ‖1 / n‖.

theorem PowerSeries.onOpenDisc_one_of_norm_coeff_le {K : Type u_1} [NormedField K] [CharZero K] {f : PowerSeries K} (h : ∀ (n : ℕ), ‖(coeff n) f‖ ≤ ‖(↑n)⁻¹‖) : OnOpenDisc 1 f

A series whose coefficient norms are bounded by the norms of inverse natural numbers lies on the open unit disc.

theorem PowerSeries.onOpenDisc_log {K : Type u_1} [NormedField K] [CharZero K] : OnOpenDisc 1 (log K)

Over a normed field of characteristic zero, the logarithm series log (1 + X) lies on the open unit disc.