Ordered boundary limits of Dirichlet series at s = 1

At the boundary point s = 1 of the half-plane 1 < re s, a Dirichlet series with coefficients a : ℕ → ℂ is studied through the ordered partial sums ∑ n ∈ Finset.Icc 1 N, a n / n. Their limit, when it exists, is a conditional limit of finite cutoffs: it says nothing about unconditional summability at 1 or about the totalized value LSeries a 1. This file collects the basic facts about such limits that do not depend on how the limit was obtained.

• Abelian theorem. If the ordered sums tend to L and the series converges absolutely on 1 < σ, then LSeries a σ → L as the real number σ decreases to 1. The proof writes LSeries a (1 + ε) as ε ∫_1^∞ t ^ (-ε - 1) S(t) dt, with S(t) the partial sum up to t, using Mathlib's LSeries_eq_mul_integral, and averages S(t) → L against these weights.
• Uniqueness. Consequently the ordered limit equals F 1 for every function F that sums the series at real σ > 1 and satisfies F σ → F 1 as σ → 1⁺, for instance any extension continuous at 1. Two continuous extensions of the series to the closed half-plane σ ≤ re s agree there.
• Linearity. Ordered limits are additive and homogeneous in the coefficients.

Limits over real cutoffs ∑ n ≤ x are equivalent to those over natural cutoffs by TauCeti.tendsto_comp_natFloor_iff.

The Abelian theorem is classical (see Hardy and Riesz); its proof here follows the integral representation and the split of the range of integration used in Mathlib's LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div.

Main declarations

• TauCeti.LSeries.tendsto_LSeries_nhdsGT_one: the Abelian theorem at s = 1.
• TauCeti.LSeries.eq_of_tendsto_sum_Icc_div: the ordered limit is the boundary value of any extension that is continuous at 1 along the real axis.
• TauCeti.LSeries.eqOn_of_LSeriesHasSum: uniqueness of continuous extensions to a closed half-plane.
• TauCeti.LSeries.tendsto_sum_Icc_div_add, tendsto_sum_Icc_div_smul, tendsto_sum_Icc_div_neg, tendsto_sum_Icc_div_sub: linearity of ordered limits.

References

• G. H. Hardy and M. Riesz, The General Theory of Dirichlet's Series, Cambridge Tracts in Mathematics and Mathematical Physics 18, Cambridge University Press, 1915.

theorem TauCeti.LSeries.tendsto_LSeries_nhdsGT_one {a : ℕ → ℂ} {L : ℂ} (hlim : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L)) (hsum : ∀ (σ : ℝ), 1 < σ → LSeriesSummable a ↑σ) : Filter.Tendsto (fun (σ : ℝ) => LSeries a ↑σ) (nhdsWithin 1 (Set.Ioi 1)) (nhds L)

Abelian theorem for Dirichlet series at s = 1. If the ordered partial sums ∑ n ∈ Icc 1 N, a n / n tend to L and the Dirichlet series of a converges absolutely at every real σ > 1, then LSeries a σ → L as σ decreases to 1.

theorem TauCeti.LSeries.eq_of_tendsto_sum_Icc_div {a : ℕ → ℂ} {L : ℂ} {F : ℂ → ℂ} (hlim : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L)) (hF : Filter.Tendsto (fun (σ : ℝ) => F ↑σ) (nhdsWithin 1 (Set.Ioi 1)) (nhds (F 1))) (hseries : ∀ (σ : ℝ), 1 < σ → LSeriesHasSum a (↑σ) (F ↑σ)) : F 1 = L

Uniqueness of the ordered boundary limit. If the ordered partial sums ∑ n ∈ Icc 1 N, a n / n tend to L, and F σ is the sum of the Dirichlet series of a at every real σ > 1 with F σ → F 1 as σ decreases to 1, then F 1 = L. No holomorphy of F and no bound on a is needed; any extension continuous at 1 from the half-plane 1 < re s qualifies.

theorem TauCeti.LSeries.eqOn_of_LSeriesHasSum {a : ℕ → ℂ} {σ : ℝ} {F G : ℂ → ℂ} (hF : ContinuousOn F {s : ℂ | σ ≤ s.re}) (hG : ContinuousOn G {s : ℂ | σ ≤ s.re}) (hFa : ∀ (s : ℂ), σ < s.re → LSeriesHasSum a s (F s)) (hGa : ∀ (s : ℂ), σ < s.re → LSeriesHasSum a s (G s)) : Set.EqOn F G {s : ℂ | σ ≤ s.re}

Uniqueness of boundary extensions. Two functions continuous on the closed half-plane σ ≤ re s that both sum the Dirichlet series of a on the open half-plane σ < re s agree on the closed half-plane.

theorem TauCeti.LSeries.tendsto_sum_Icc_div_add {K : Type u_1} [DivisionRing K] [TopologicalSpace K] {a b : ℕ → K} {L L' : K} [ContinuousAdd K] (ha : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L)) (hb : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, b n / ↑n) Filter.atTop (nhds L')) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, (a + b) n / ↑n) Filter.atTop (nhds (L + L'))

Ordered boundary limits are additive in the coefficients.

theorem TauCeti.LSeries.tendsto_sum_Icc_div_smul {K : Type u_1} [DivisionRing K] [TopologicalSpace K] {a : ℕ → K} {L : K} [ContinuousMul K] (c : K) (ha : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L)) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, (c • a) n / ↑n) Filter.atTop (nhds (c • L))

Ordered boundary limits are homogeneous in the coefficients.

theorem TauCeti.LSeries.tendsto_sum_Icc_div_neg {K : Type u_1} [DivisionRing K] [TopologicalSpace K] {a : ℕ → K} {L : K} [ContinuousNeg K] (ha : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L)) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, (-a) n / ↑n) Filter.atTop (nhds (-L))

Negating the coefficients negates the ordered boundary limit.

theorem TauCeti.LSeries.tendsto_sum_Icc_div_sub {K : Type u_1} [DivisionRing K] [TopologicalSpace K] {a b : ℕ → K} {L L' : K} [ContinuousSub K] (ha : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L)) (hb : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, b n / ↑n) Filter.atTop (nhds L')) : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc 1 N, (a - b) n / ↑n) Filter.atTop (nhds (L - L'))

Ordered boundary limits are subtractive in the coefficients.