Theorem: LSeries.tendsto_atTop (EulerProducts/LSeriesUnique.lean)

State before:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))
Tactic:
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n
State after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

State before:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))
Tactic:
have hF₀ : F 0 = 0 := rfl
State after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

State before:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))
Tactic:
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := by simp only [hn, ↓reduceIte, F]
State after:
f : ℕ → ℂ
ha : 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
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

State before:
f : ℕ → ℂ
ha : 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
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))
Tactic:
have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha
State after:
f : ℕ → ℂ
ha : 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 < ⊤
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))

State before:
f : ℕ → ℂ
ha : 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 < ⊤
⊢ Tendsto (fun x => LSeries f ↑x) atTop (nhds (f 1))
Tactic:
simp_rw [← LSeries_congr _ hF]
State after:
f : ℕ → ℂ
ha : 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 < ⊤
⊢ Tendsto (fun x => LSeries (fun {n} => F n) ↑x) atTop (nhds (f 1))

State before:
f : ℕ → ℂ
ha : 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 < ⊤
⊢ Tendsto (fun x => LSeries (fun {n} => F n) ↑x) atTop (nhds (f 1))
Tactic:
convert LSeries.tendsto_pow_mul_atTop (n := 0) (fun _ hm ↦ Nat.le_zero.mp hm ▸ hF₀) ha' using 1
State after:
case h.e'_3
f : ℕ → ℂ
ha : 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 < ⊤
⊢ (fun x => LSeries (fun {n} => F n) ↑x) = fun x => (↑0 + 1) ^ ↑x * LSeries F ↑x

State before:
case h.e'_3
f : ℕ → ℂ
ha : 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 < ⊤
⊢ (fun x => LSeries (fun {n} => F n) ↑x) = fun x => (↑0 + 1) ^ ↑x * LSeries F ↑x
Tactic:
simp only [Nat.cast_zero, zero_add, one_cpow, one_mul]
State after:
no goals

State before:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n => if n = 0 then 0 else f n
hF₀ : F 0 = 0
n : ℕ
hn : n ≠ 0
⊢ F n = f n
Tactic:
simp only [hn, ↓reduceIte, F]
State after:
no goals