-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- 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. -/
lemma LSeries_eventually_eq_zero_iff' {f : ℕ → ℂ} :
    (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] 0 ↔ (∀ n ≠ 0, f n = 0) ∨ abscissaOfAbsConv f = ⊤

Proof state:
f : ℕ → ℂ
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤

Tactic:
by_cases h : abscissaOfAbsConv f = ⊤ <;> simp [h]

Result:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0

case neg
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ ∀ (n : ℕ), F n = 0

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun x => 0) atTop (nhds (F 0))

Tactic:
simp [hF₀]

Result:
no goals

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
⊢ ∀ (n : ℕ), F n = 0

Tactic:
have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr x hF

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
⊢ ∀ (n : ℕ), F n = 0

Proof state:
case neg
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ Eventually.of_forall fun x ↦ ?_⟩

Result:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), ¬n = 0 → f n = 0
x : ℝ
⊢ (fun x => LSeries f ↑x) x = 0 x

Proof state:
case intro
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
s : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x => LSeries f ↑x) 0 s
⊢ ∃ s ∈ atTop, Set.EqOn (fun x => ↑n ^ ↑x * LSeries f ↑x) (fun x => 0) s

Tactic:
exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩

Result:
no goals

Proof state:
case neg.refine_1.ind.zero
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun x => ↑0 ^ ↑x * LSeries F ↑x) atTop (nhds (F 0))

Tactic:
exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]

Result:
no goals

Proof state:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x => LSeries f ↑x) x = 0 x

Tactic:
simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]

Result:
no goals

Proof state:
case neg.refine_1.ind.succ
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n + 1, F m = 0
⊢ Tendsto (fun x => ↑(n + 1) ^ ↑x * LSeries F ↑x) atTop (nhds (F (n + 1)))

Tactic:
simpa using LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
  Ne.lt_top ha

Result:
no goals

Proof state:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ (fun x => ↑n ^ ↑x * LSeries f ↑x) =ᶠ[atTop] fun x => 0

Tactic:
rw [eventuallyEq_iff_exists_mem] at H ⊢

Result:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∃ s ∈ atTop, Set.EqOn (fun x => LSeries f ↑x) 0 s
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ ∃ s ∈ atTop, Set.EqOn (fun x => ↑n ^ ↑x * LSeries f ↑x) (fun x => 0) s

Proof state:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
⊢ F n = 0

Tactic:
induction n using Nat.strongRecOn with | ind n ih =>
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

Result:
no goals

Proof state:
case neg.refine_1.ind
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x => LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x => ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x => 0
n : ℕ
ih : ∀ m < n, F m = 0
⊢ Tendsto (fun x => ↑n ^ ↑x * LSeries F ↑x) atTop (nhds (F n))

Tactic:
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

Result:
no goals

Proof state:
case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), ¬n = 0 → f n = 0
x : ℝ
⊢ (fun x => LSeries f ↑x) x = 0 x

Tactic:
simp [LSeries_congr x fun {n} ↦ H n, show (fun _ : ℕ ↦ (0 : ℂ)) = 0 from rfl]

Result:
no goals