Majorants of entire power series

This file supplies the two majorants that control Coleman's spectral transform D(B, F) of an entire series F with F(0) = 1 along an entire series B with B(0) = 0.

Newton majorants. A power series F = ∑ aⱼ Tʲ over a normed ring with ‖a₀‖ ≤ 1 is entire exactly when its coefficients are dominated by the partial products of a positive antitone null sequence ρ:

‖aⱼ‖ ≤ ∏ i < j, ρᵢ (PowerSeries.isEntire_iff_exists_newtonMajorant).

One direction holds since ‖aⱼ‖ |r| ^ j ≤ ∏ i < j, |ρᵢ| |r| and the factors |ρᵢ| |r| tend to zero (PowerSeries.isEntire_of_norm_coeff_le_prod). For the other, the j-th roots ‖aⱼ‖ ^ (1 / j) of the coefficients of an entire series tend to zero (PowerSeries.IsEntire.tendsto_norm_coeff_rpow_inv_natCast), and ρᵢ is the supremum of the roots of index greater than i, plus 2⁻ⁱ to make it positive. In terms of v = -log ‖·‖, with the convention v(0) = +∞, the bound says that the points (j, v(aⱼ)) lie above the convex polygon with slopes -log ρᵢ, whence the name; no valuation is needed here.

Coleman majorants. For a power series B = ∑ bₘ Tᵐ and a radius r, the Coleman majorant is the supremum of the weighted coefficients of positive degree,

β_B(r) = sup_{m ≥ 1} ‖bₘ‖ rᵐ (PowerSeries.colemanMajorant),

that is, for r ≥ 0, the Gauss norm of B - B(0) at radius r.

If B is restricted at the radius r, the supremum is finite, so every weighted coefficient ‖bₘ‖ rᵐ with m ≥ 1 is bounded by β_B(r) (PowerSeries.norm_coeff_succ_mul_pow_le_colemanMajorant). If B is restricted at a radius s > 0, then β_B is monotone on [0, s] and, since the constant term is omitted, β_B(r) ≤ (r / s) β_B(s) for 0 ≤ r ≤ s; so β_B(r) tends to zero with r (PowerSeries.tendsto_colemanMajorant). Composed with a Newton majorant ρ of F, the products ∏ i < k, β_B(ρᵢ) therefore again form the coefficient bounds of an entire series. In Coleman's construction, these products bound the coefficients of the spectral transform D(B, F), which is therefore entire.

Main definitions

• PowerSeries.colemanMajorant: β_B(r) = sup_{m ≥ 1} ‖bₘ‖ rᵐ.

Main results

• PowerSeries.IsEntire.tendsto_norm_coeff_rpow_inv_natCast: the n-th roots of the coefficient norms of an entire series tend to zero.
• PowerSeries.IsEntire.exists_newtonMajorant and PowerSeries.isEntire_of_norm_coeff_le_prod: the two directions of PowerSeries.isEntire_iff_exists_newtonMajorant.
• PowerSeries.IsEntire.exists_newtonMajorant_mul: a Newton majorant dominating the convolution of the coefficient norms of two entire series.
• PowerSeries.norm_coeff_succ_mul_pow_le_colemanMajorant and PowerSeries.colemanMajorant_le: β_B(r) is the least upper bound of the weighted coefficients of positive degree.
• PowerSeries.monotoneOn_colemanMajorant and PowerSeries.colemanMajorant_le_div_mul: monotonicity, and the linear bound near 0.
• PowerSeries.tendsto_colemanMajorant: β_B(ρᵢ) → 0 whenever ρᵢ → 0 with ρᵢ ≥ 0.
• PowerSeries.norm_coeff_trunc_le_prod and PowerSeries.norm_coeff_trunc_succ_mul_pow_le_colemanMajorant: truncations of F and B obey the same Newton and Coleman majorants.
• PowerSeries.tendsto_colemanMajorant_sub_trunc: the majorants β_(B - trunc L B)(r) of the tails of a series restricted at r tend to zero as L → ∞.

References

• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A.

theorem PowerSeries.IsEntire.tendsto_norm_coeff_rpow_inv_natCast {R : Type u_1} [NormedRing R] {F : PowerSeries R} (hF : F.IsEntire) : Filter.Tendsto (fun (n : ℕ) => ‖(coeff n) F‖ ^ (↑n)⁻¹) Filter.atTop (nhds 0)

Cauchy–Hadamard for entire series. The n-th roots ‖aₙ‖ ^ (1 / n) of the coefficient norms of an entire series tend to zero.

theorem PowerSeries.IsEntire.exists_newtonMajorant {R : Type u_1} [NormedRing R] {F : PowerSeries R} (hF : F.IsEntire) (hF0 : ‖(coeff 0) F‖ ≤ 1) : ∃ (ρ : ℕ → ℝ), (∀ (i : ℕ), 0 < ρ i) ∧ Antitone ρ ∧ Filter.Tendsto ρ Filter.atTop (nhds 0) ∧ ∀ (j : ℕ), ‖(coeff j) F‖ ≤ ∏ i ∈ Finset.range j, ρ i

Newton majorants of entire series. The coefficients of an entire series ∑ aⱼ Tʲ with ‖a₀‖ ≤ 1, for instance with a₀ = 1, are dominated by the partial products of a positive antitone sequence tending to zero: ‖aⱼ‖ ≤ ∏ i < j, ρᵢ.

theorem PowerSeries.isEntire_of_norm_coeff_le_prod {R : Type u_1} [NormedRing R] {F : PowerSeries R} {σ : ℕ → ℝ} (hσ : Filter.Tendsto σ Filter.atTop (nhds 0)) (hF : ∀ (j : ℕ), ‖(coeff j) F‖ ≤ ∏ i ∈ Finset.range j, σ i) : F.IsEntire

A power series whose coefficients are dominated by the partial products of a sequence tending to zero, ‖aⱼ‖ ≤ ∏ i < j, σᵢ, is entire.

theorem PowerSeries.isEntire_iff_exists_newtonMajorant {R : Type u_1} [NormedRing R] {F : PowerSeries R} (hF0 : ‖(coeff 0) F‖ ≤ 1) : F.IsEntire ↔ ∃ (ρ : ℕ → ℝ), (∀ (i : ℕ), 0 < ρ i) ∧ Antitone ρ ∧ Filter.Tendsto ρ Filter.atTop (nhds 0) ∧ ∀ (j : ℕ), ‖(coeff j) F‖ ≤ ∏ i ∈ Finset.range j, ρ i

Newton majorants characterise entire series. A power series ∑ aⱼ Tʲ with ‖a₀‖ ≤ 1 is entire exactly when ‖aⱼ‖ ≤ ∏ i < j, ρᵢ for a positive antitone sequence ρ tending to zero.

theorem PowerSeries.IsEntire.exists_newtonMajorant_mul {R : Type u_1} [NormedRing R] {F G : PowerSeries R} (hF : F.IsEntire) (hG : G.IsEntire) (hF0 : ‖(coeff 0) F‖ ≤ 1) (hG0 : ‖(coeff 0) G‖ ≤ 1) : ∃ (ρ : ℕ → ℝ), (∀ (i : ℕ), 0 < ρ i) ∧ Antitone ρ ∧ Filter.Tendsto ρ Filter.atTop (nhds 0) ∧ ∀ (j : ℕ), ∑ x ∈ Finset.antidiagonal j, ‖(coeff x.1) F‖ * ‖(coeff x.2) G‖ ≤ ∏ i ∈ Finset.range j, ρ i

Newton majorants of products. For entire series F = ∑ aⱼ Tʲ and G = ∑ bⱼ Tʲ with ‖a₀‖ ≤ 1 and ‖b₀‖ ≤ 1, one positive antitone sequence ρ tending to zero dominates the convolution of their coefficient norms: ∑ i + l = j, ‖aᵢ‖ ‖bₗ‖ ≤ ∏ i < j, ρᵢ. It is therefore a Newton majorant of F * G and of every product of truncations of F and G.

theorem PowerSeries.norm_coeff_trunc_le_prod {R : Type u_1} [NormedRing R] {F : PowerSeries R} {ρ : ℕ → ℝ} (hρ₀ : ∀ (i : ℕ), 0 ≤ ρ i) (hF : ∀ (j : ℕ), ‖(coeff j) F‖ ≤ ∏ i ∈ Finset.range j, ρ i) (b j : ℕ) : ‖((trunc b) F).coeff j‖ ≤ ∏ i ∈ Finset.range j, ρ i

Truncation preserves a Newton majorant: ‖coeff j (trunc b F)‖ ≤ ∏ i < j, ρ i whenever ‖coeff j F‖ ≤ ∏ i < j, ρ i for all j and ρ is nonnegative.

noncomputable def PowerSeries.colemanMajorant {R : Type u_1} [NormedRing R] (B : PowerSeries R) (r : ℝ) : ℝ

The Coleman majorant β_B(r) = sup_{m ≥ 1} ‖bₘ‖ rᵐ of a power series B = ∑ bₘ Tᵐ at the radius r. For r ≥ 0 it is the Gauss norm of B - B(0) (PowerSeries.colemanMajorant_eq_gaussNorm). It is a genuine supremum whenever the weighted coefficients ‖bₘ‖ rᵐ are bounded above, for instance when B is restricted at the radius r (PowerSeries.norm_coeff_succ_mul_pow_le_colemanMajorant); only for an unbounded family does it take the junk value 0 of an unbounded real supremum.

theorem PowerSeries.colemanMajorant_def {R : Type u_1} [NormedRing R] (B : PowerSeries R) (r : ℝ) : B.colemanMajorant r = ⨆ (m : ℕ), ‖(coeff (m + 1)) B‖ * r ^ (m + 1)

The defining supremum of the Coleman majorant.

theorem PowerSeries.colemanMajorant_nonneg {R : Type u_1} [NormedRing R] (B : PowerSeries R) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ B.colemanMajorant r

The Coleman majorant at a nonnegative radius is nonnegative.

theorem PowerSeries.colemanMajorant_eq_gaussNorm {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r : ℝ} (hr : 0 ≤ r) : B.colemanMajorant r = gaussNorm norm r (B - C ((coeff 0) B))

At a nonnegative radius, the Coleman majorant of B is the Gauss norm of B - B(0).

theorem PowerSeries.colemanMajorant_le {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r c : ℝ} (h : ∀ (m : ℕ), ‖(coeff (m + 1)) B‖ * r ^ (m + 1) ≤ c) : B.colemanMajorant r ≤ c

The Coleman majorant is at most any bound for the weighted coefficients of positive degree.

theorem PowerSeries.norm_coeff_succ_mul_pow_le_colemanMajorant {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r : ℝ} (hB : IsRestricted r B) (m : ℕ) : ‖(coeff (m + 1)) B‖ * r ^ (m + 1) ≤ B.colemanMajorant r

The Coleman majorant bounds the coefficients. If B is restricted at the radius r, every weighted coefficient ‖bₘ‖ rᵐ of positive degree is at most β_B(r).

theorem PowerSeries.colemanMajorant_le_colemanMajorant {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r s : ℝ} (hB : IsRestricted s B) (hr : 0 ≤ r) (hrs : r ≤ s) : B.colemanMajorant r ≤ B.colemanMajorant s

The Coleman majorant is monotone in the radius below a radius of restrictedness.

theorem PowerSeries.monotoneOn_colemanMajorant {R : Type u_1} [NormedRing R] {B : PowerSeries R} (hB : B.IsEntire) : MonotoneOn B.colemanMajorant (Set.Ici 0)

The Coleman majorant of an entire series is monotone on the nonnegative radii.

theorem PowerSeries.colemanMajorant_le_div_mul {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r s : ℝ} (hB : IsRestricted s B) (hs : 0 < s) (hr : 0 ≤ r) (hrs : r ≤ s) : B.colemanMajorant r ≤ r / s * B.colemanMajorant s

Linear bound near zero. Since the constant term is omitted, β_B(r) ≤ (r / s) β_B(s) for 0 ≤ r ≤ s when B is restricted at the radius s > 0.

theorem PowerSeries.tendsto_colemanMajorant {R : Type u_1} [NormedRing R] {B : PowerSeries R} {ι : Type u_2} {l : Filter ι} {ρ : ι → ℝ} {s : ℝ} (hB : IsRestricted s B) (hs : 0 < s) (hρ0 : ∀ (i : ι), 0 ≤ ρ i) (hρ : Filter.Tendsto ρ l (nhds 0)) : Filter.Tendsto (fun (i : ι) => B.colemanMajorant (ρ i)) l (nhds 0)

Decay of the Coleman majorant. If B is restricted at some positive radius, then β_B(ρᵢ) tends to zero along every nonnegative family of radii ρᵢ tending to zero.

theorem PowerSeries.colemanMajorant_trunc_le {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r : ℝ} (hB : IsRestricted r B) (hr : 0 ≤ r) (n : ℕ) : (↑((trunc n) B)).colemanMajorant r ≤ B.colemanMajorant r

Truncation does not increase the Coleman majorant at a nonnegative radius.

theorem PowerSeries.norm_coeff_trunc_succ_mul_pow_le_colemanMajorant {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r : ℝ} (hB : IsRestricted r B) (hr : 0 ≤ r) (a j : ℕ) : ‖((trunc a) B).coeff (j + 1)‖ * r ^ (j + 1) ≤ B.colemanMajorant r

The weighted coefficients of positive degree of a truncation of B are bounded by the Coleman majorant of B at any nonnegative radius where B is restricted.

theorem PowerSeries.tendsto_colemanMajorant_sub_trunc {R : Type u_1} [NormedRing R] {B : PowerSeries R} {r : ℝ} (hB : IsRestricted r B) : Filter.Tendsto (fun (L : ℕ) => (B - ↑((trunc L) B)).colemanMajorant r) Filter.atTop (nhds 0)

Decay of the tail majorants. If B is restricted at the radius r, the Coleman majorants of its tails B - trunc L B, the suprema sup_{m ≥ max L 1} ‖bₘ‖ rᵐ, tend to zero as L → ∞.

@[simp]

theorem PowerSeries.colemanMajorant_zero_right {R : Type u_1} [NormedRing R] (B : PowerSeries R) : B.colemanMajorant 0 = 0

The Coleman majorant at the radius 0 vanishes.

@[simp]

theorem PowerSeries.colemanMajorant_C {R : Type u_1} [NormedRing R] (a : R) (r : ℝ) : (C a).colemanMajorant r = 0

The Coleman majorant ignores the constant term.

@[simp]

theorem PowerSeries.colemanMajorant_zero {R : Type u_1} [NormedRing R] (r : ℝ) : colemanMajorant 0 r = 0

The Coleman majorant of the zero series vanishes.

@[simp]

theorem PowerSeries.colemanMajorant_X_pow {R : Type u_1} [NormedRing R] [NormOneClass R] {k : ℕ} (hk : k ≠ 0) {r : ℝ} (hr : 0 ≤ r) : (X ^ k).colemanMajorant r = r ^ k

The Coleman majorant of a monomial Tᵏ of positive degree is rᵏ at a radius r ≥ 0.

@[simp]

theorem PowerSeries.colemanMajorant_X {R : Type u_1} [NormedRing R] [NormOneClass R] {r : ℝ} (hr : 0 ≤ r) : X.colemanMajorant r = r

The Coleman majorant of T is the radius r ≥ 0 itself.