internlm/Lean-Github huggingface dataset:
Theorem: LSeries.tendsto_atTop
Proof 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
Proof 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))
Theorem: LSeries.tendsto_atTop
Proof 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
Proof 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))
Theorem: LSeries.tendsto_atTop
Proof 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]
Proof 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))
Theorem: LSeries.tendsto_atTop
Proof 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
Proof 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))
Theorem: LSeries.tendsto_atTop
Proof 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]
Proof 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))
Theorem: LSeries.tendsto_atTop
Proof 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
Proof 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
Theorem: LSeries.tendsto_atTop
Proof 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]
Proof state after:
no goals
Theorem: LSeries.tendsto_atTop
Proof 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]
Proof state after:
no goals
Theorem: LSeries_eq_zero_of_abscissaOfAbsConv_eq_top
Proof state before:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0
Tactic:
ext s
Proof state after:
case h
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s
Theorem: LSeries_eq_zero_of_abscissaOfAbsConv_eq_top
Proof state before:
case h
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s
Tactic:
exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
  h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
f : ℕ → ℂ
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0 ↔ (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ abscissaOfAbsConv f = ⊤
Tactic:
by_cases h : abscissaOfAbsConv f = ⊤ <;> simp only [h, or_true, or_false, iff_true]
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ (fun x => LSeries f ↑x) =ᶠ[atTop] 0
Tactic:
refine eventually_of_forall ?_
Proof state after:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x => LSeries f ↑x) x = 0 x
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
case pos
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x => LSeries f ↑x) x = 0 x
Tactic:
simp only [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h, Pi.zero_apply, forall_const]
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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 ↦ ?_⟩
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
Tactic:
have hF₀ : F 0 = 0 := rfl
Proof state after:
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
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := by simp only [hn, ↓reduceIte, F]
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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 by
  peel hF with n hn h
  exact (this n ▸ h).symm
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
Tactic:
have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
Tactic:
have H' (n : ℕ) : (fun x : ℝ ↦ (n ^ (x : ℂ)) * LSeries F x) =ᶠ[atTop] (fun _ ↦ 0) := by
  simp only [h']
  rw [eventuallyEq_iff_exists_mem] at H ⊢
  peel H with s hs
  refine ⟨hs.1, fun x hx ↦ ?_⟩
  simp only [hs.2 hx, Pi.zero_apply, mul_zero]
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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:
intro n
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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.strongInductionOn with n ih
Proof state after:
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
⊢ F n = 0
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
⊢ F n = 0
Tactic:
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
Proof state after:
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))
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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 =>
    refine Tendsto.congr' (H' 0).symm ?_
    simp only [zero_eq, hF₀, tendsto_const_nhds_iff]
| succ n =>
    simp only [succ_eq_add_one, cast_add, cast_one]
    exact LSeries.tendsto_pow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <| Ne.lt_top ha
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
n : ℕ
hn : n ≠ 0
⊢ F n = f n
Tactic:
simp only [hn, ↓reduceIte, F]
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
this : ∀ (n : ℕ), F n = 0
⊢ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
peel hF with n hn h
Proof state after:
case h.h
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
this : ∀ (n : ℕ), F n = 0
n : ℕ
hn : n ≠ 0
h : F n = f n
⊢ f n = 0
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
case h.h
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
this : ∀ (n : ℕ), F n = 0
n : ℕ
hn : n ≠ 0
h : F n = f n
⊢ f n = 0
Tactic:
exact (this n ▸ h).symm
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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:
simp only [h']
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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 ⊢
Proof state after:
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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
Tactic:
peel H with s hs
Proof state after:
case h
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 : 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
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
case h
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 : 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:
refine ⟨hs.1, fun x hx ↦ ?_⟩
Proof state after:
case h
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 : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x => LSeries f ↑x) 0 s
x : ℝ
hx : x ∈ s
⊢ (fun x => ↑n ^ ↑x * LSeries f ↑x) x = (fun x => 0) x
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
case h
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 : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x => LSeries f ↑x) 0 s
x : ℝ
hx : x ∈ s
⊢ (fun x => ↑n ^ ↑x * LSeries f ↑x) x = (fun x => 0) x
Tactic:
simp only [hs.2 hx, Pi.zero_apply, mul_zero]
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
this : Tendsto (fun x => ↑n ^ ↑x * LSeries F ↑x) atTop (nhds (F n))
⊢ F n = 0
Tactic:
replace this := this.congr' <| H' n
Proof state after:
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
this : Tendsto (fun x => 0) atTop (nhds (F n))
⊢ F n = 0
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
this : Tendsto (fun x => 0) atTop (nhds (F n))
⊢ F n = 0
Tactic:
simp only [tendsto_const_nhds_iff] at this
Proof state after:
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
this : 0 = F n
⊢ F n = 0
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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
this : 0 = F n
⊢ F n = 0
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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:
refine Tendsto.congr' (H' 0).symm ?_
Proof state after:
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) atTop (nhds (F 0))
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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) atTop (nhds (F 0))
Tactic:
simp only [zero_eq, hF₀, tendsto_const_nhds_iff]
Proof state after:
no goals
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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:
simp only [succ_eq_add_one, cast_add, cast_one]
Proof state after:
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)))
Theorem: LSeries_eventually_eq_zero_iff'
Proof state before:
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:
exact LSeries.tendsto_pow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <| Ne.lt_top ha
Proof state after:
no goals