English
Assuming f(0)=0, LSeries f = 0 if and only if f = 0 or abscissaOfAbsConv f = ∞.
Русский
Пусть f(0)=0. Тогда LSeries f = 0 тогда и только тогда, когда f = 0 или abscissaOfAbsConv f = ∞.
LaTeX
$$$$ \text{If } f(0)=0, \; LSeries f = 0 \iff f = 0 \lor \operatorname{abscissaOfAbsConv}(f) = \top. $$$$
Lean4
/-- 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_eq_zero_iff {f : ℕ → ℂ} (hf : f 0 = 0) : LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤ :=
by
by_cases h : abscissaOfAbsConv f = ⊤
· simpa [h] using LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h
· simp only [h, or_false]
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩
convert (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h
· refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩
ext (- | m)
· simp [hf]
· simp [H']
· simpa only [H] using Filter.EventuallyEq.rfl
