A converging L-series determines its coefficients

We show that two functions f and g : ℕ → ℂ whose L-series agree and both converge somewhere must agree on all nonzero arguments. See LSeries_eq_iff_of_abscissaOfAbsConv_lt_top and LSeries_injOn.

theorem LSeries.abscissaOfAbsConv_add_le (f g : ℕ → ℂ) : LSeries.abscissaOfAbsConv (f + g) ≤ LSeries.abscissaOfAbsConv f ⊔ LSeries.abscissaOfAbsConv g

The abscissa of absolute convergence of f + g is at most the maximum of those of f and g.

theorem LSeries.abscissaOfAbsConv_sub_le (f g : ℕ → ℂ) : LSeries.abscissaOfAbsConv (f - g) ≤ LSeries.abscissaOfAbsConv f ⊔ LSeries.abscissaOfAbsConv g

The abscissa of absolute convergence of f - g is at most the maximum of those of f and g.

theorem LSeries.tendsto_cpow_mul_atTop {f : ℕ → ℂ} {n : ℕ} (h : ∀ m ≤ n, f m = 0) (ha : LSeries.abscissaOfAbsConv f < ⊤) : Filter.Tendsto (fun (x : ℝ) => (↑n + 1) ^ ↑x * LSeries f ↑x) Filter.atTop (nhds (f (n + 1)))

If the coefficients f m of an L-series are zero for m ≤ n and the L-series converges at some point, then f (n+1) is the limit of (n+1)^x * LSeries f x as x → ∞.

theorem LSeries.tendsto_atTop {f : ℕ → ℂ} (ha : LSeries.abscissaOfAbsConv f < ⊤) : Filter.Tendsto (fun (x : ℝ) => LSeries f ↑x) Filter.atTop (nhds (f 1))

If the L-series of f converges at some point, then f 1 is the limit of LSeries f x as x → ∞.

theorem LSeries_eq_zero_of_abscissaOfAbsConv_eq_top {f : ℕ → ℂ} (h : LSeries.abscissaOfAbsConv f = ⊤) : LSeries f = 0

theorem LSeries_eventually_eq_zero_iff' {f : ℕ → ℂ} : (fun (x : ℝ) => LSeries f ↑x) =ᶠ[Filter.atTop] 0 ↔ (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ LSeries.abscissaOfAbsConv f = ⊤

The LSeries of f is zero for large real arguments if and only if either f n = 0 for all n ≠ 0 or the L-series converges nowhere.

theorem LSeries_eq_zero_iff {f : ℕ → ℂ} (hf : f 0 = 0) : LSeries f = 0 ↔ f = 0 ∨ LSeries.abscissaOfAbsConv f = ⊤

Assuming f 0 = 0, the LSeries of f is zero if and only if either f = 0 or the L-series converges nowhere.

theorem LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq {f g : ℕ → ℂ} (hf : LSeries.abscissaOfAbsConv f < ⊤) (hg : LSeries.abscissaOfAbsConv g < ⊤) (h : (fun (x : ℝ) => LSeries f ↑x) =ᶠ[Filter.atTop] fun (x : ℝ) => LSeries g ↑x) : (fun (x : ℝ) => LSeries (f - g) ↑x) =ᶠ[Filter.atTop] 0

If the LSeries of f and of g converge somewhere and agree on large real arguments, then the L-series of f - g is zero for large real arguments.

theorem LSeries.eq_of_LSeries_eventually_eq {f g : ℕ → ℂ} (hf : LSeries.abscissaOfAbsConv f < ⊤) (hg : LSeries.abscissaOfAbsConv g < ⊤) (h : (fun (x : ℝ) => LSeries f ↑x) =ᶠ[Filter.atTop] fun (x : ℝ) => LSeries g ↑x) {n : ℕ} (hn : n ≠ 0) : f n = g n

If the LSeries of f and of g converge somewhere and agree on large real arguments, then f n = g n whenever n ≠ 0.

theorem LSeries_eq_iff_of_abscissaOfAbsConv_lt_top {f g : ℕ → ℂ} (hf : LSeries.abscissaOfAbsConv f < ⊤) (hg : LSeries.abscissaOfAbsConv g < ⊤) : LSeries f = LSeries g ↔ ∀ (n : ℕ), n ≠ 0 → f n = g n

If the LSeries of f and of g both converge somewhere, then they are equal if and only if f n = g n whenever n ≠ 0.

theorem LSeries_injOn : Set.InjOn LSeries {f : ℕ → ℂ | f 0 = 0 ∧ LSeries.abscissaOfAbsConv f < ⊤}

The map f ↦ LSeries f is injective on functions f such that f 0 = 0 and the L-series of f converges somewhere.