English
The L-series f is eventually zero as x → ∞ if and only if either f(n)=0 for all n ≠ 0 or abscissaOfAbsConv f = ∞.
Русский
L-порядок f становится равным нулю на бесконечности тогда и только тогда, когда либо f(n)=0 для всех n ≠ 0, либо абсцисса абсолютной сходимости равна бесконечности.
LaTeX
$$$$ (\mathrm{LSeries} f)(x) = 0 \text{ for large } x \quad\Longleftrightarrow\quad (\forall n \neq 0, f(n)=0) \lor \operatorname{abscissaOfAbsConv}(f) = \top. $$$$
Lean4
/-- 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_eventually_eq_zero_iff' {f : ℕ → ℂ} :
(fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] 0 ↔ (∀ n ≠ 0, f n = 0) ∨ abscissaOfAbsConv f = ⊤ :=
by
by_cases h : abscissaOfAbsConv f = ⊤
· simpa [h] using Eventually.of_forall <| by simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]
· simp only [ne_eq, h, or_false]
refine ⟨fun H ↦ ?_, fun H ↦ Eventually.of_forall fun x ↦ ?_⟩
· let F (n : ℕ) : ℂ := if n = 0 then 0 else f n
have hF₀ : F 0 = 0 := rfl
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)
have ha : ¬abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr hF x
have H' (n : ℕ) : (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) =ᶠ[atTop] fun _ ↦ 0 :=
by
simp only [h']
rw [eventuallyEq_iff_exists_mem] at H ⊢
obtain ⟨s, hs⟩ := H
exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩
intro n
induction n using Nat.strongRecOn with
| ind n ih =>
-- it suffices to show that `n ^ x * LSeries F x` tends to `F n` as `x` tends to `∞`
suffices Tendsto (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) atTop (nhds (F n))
by
replace this := this.congr' <| H' n
simp only [tendsto_const_nhds_iff] at this
exact this.symm
cases n with
| zero => exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]
| succ n => simpa using LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <| Ne.lt_top ha
· simp [LSeries_congr (fun {n} ↦ H n) x, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]
