The Wiener--Ikehara theorem for coefficients in an ordered vector space

Let E be a finite-dimensional real normed space with a partial order compatible with its module structure and a closed positive cone; for instance ι → ℝ with the coordinatewise order for a finite type ι, or any finite-dimensional ordered real normed algebra with closed positive cone. For coefficients a n ∈ E that are eventually nonnegative, this file deduces the asymptotic x⁻¹ ∑_{1 ≤ n ≤ x} a n → κ in E from the scalar theorem TauCeti.LSeries.wienerIkehara_of_eventually_nonneg.

Mathlib's LSeries has complex coefficients, so the analytic input is stated one monotone continuous linear functional φ i at a time, for a family whose span contains every monotone continuous linear functional (for ι → ℝ, the coordinate projections): the real coefficients φ i (a n) are eventually nonnegative, and their Dirichlet series, less φ i κ / (s - 1), is required to extend continuously to Re s ≥ 1. The scalar theorem then gives the asymptotic for every φ i (a n), and by linearity for every functional in their span. Monotone continuous functionals separate the points of E because its positive cone is closed (TauCeti.eq_iff_forall_monotone_dual_eq, a consequence of Farkas' lemma), so evaluation at them is an injective linear map from the finite-dimensional space E, hence a closed embedding, and the scalar limits assemble to the limit in E (TauCeti.tendsto_iff_forall_monotone_dual).

Finite dimensionality is what turns convergence against each functional into convergence in E. Closedness of the positive cone is what makes the monotone functionals separate points: for the lexicographic order on ℝ², whose positive cone is not closed, the monotone continuous linear functionals are the nonnegative multiples of the first coordinate, so the hypotheses say nothing about the second coordinates of the a n.

Main results

• TauCeti.LSeries.wienerIkehara_of_forall_monotone_dual: the Wiener--Ikehara theorem for eventually nonnegative coefficients in a finite-dimensional ordered real normed space with closed positive cone.

References

• J. Korevaar, Tauberian Theory: A Century of Developments, Chapter III.

theorem TauCeti.LSeries.wienerIkehara_of_forall_monotone_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [OrderClosedTopology E] {ι : Type u_2} {φ : ι → StrongDual ℝ E} (hφ : ∀ (i : ι), Monotone ⇑(φ i)) (hspan : ∀ (ψ : StrongDual ℝ E), Monotone ⇑ψ → ψ ∈ Submodule.span ℝ (Set.range φ)) {a : ℕ → E} {κ : E} (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n) (hFG : ∀ (i : ι), ∃ (F : ℂ → ℂ) (G : ℂ → ℂ), (∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun (n : ℕ) => ↑((φ i) (a n))) s (F s)) ∧ ContinuousOn G {s : ℂ | 1 ≤ s.re} ∧ ∀ (s : ℂ), 1 < s.re → G s = F s - ↑((φ i) κ) / (s - 1)) : Filter.Tendsto (fun (x : ℝ) => x⁻¹ • ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds κ)

The Wiener--Ikehara theorem for coefficients in an ordered vector space. Let E be a finite-dimensional ordered real normed space with closed positive cone, and let a n ∈ E satisfy 0 ≤ a n for all large n. Let φ i be a family of monotone continuous linear functionals on E whose span contains every monotone continuous linear functional. Suppose that for each i, the Dirichlet series of the real coefficients φ i (a n) has sum F s on Re s > 1 and there is a function G continuous on Re s ≥ 1 with G s = F s - φ i κ / (s - 1) on Re s > 1. Then x⁻¹ ∑_{1 ≤ n ≤ x} a n → κ in E as x → ∞.

For E = ι → ℝ one may take the coordinate projections, for E = ℝ the identity alone, and in general all monotone continuous linear functionals.