case pos
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

case neg
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
by_cases hf : Summable f
case pos
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
h₀ : (fun i => (∑' (i : ℕ), f i) - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
case pos
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
have h₀ : (fun i => (∑' i, f i) - ∑ j in range i, f j) = fun i => ∑' k : ℕ, f (k + i) := by
  ext1 i
  rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf]
case pos
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
h₀ : (fun i => (∑' (i : ℕ), f i) - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
h₁ : Tendsto (fun x => ∑' (i : ℕ), f i) atTop (𝓝 (∑' (i : ℕ), f i))
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
case pos
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
h₀ : (fun i => (∑' (i : ℕ), f i) - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
have h₁ : Tendsto (fun _ : ℕ => ∑' i, f i) atTop (𝓝 (∑' i, f i)) := tendsto_const_nhds
no goals
case pos
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
h₀ : (fun i => (∑' (i : ℕ), f i) - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
h₁ : Tendsto (fun x => ∑' (i : ℕ), f i) atTop (𝓝 (∑' (i : ℕ), f i))
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
simpa only [h₀, sub_self] using Tendsto.sub h₁ hf.hasSum.tendsto_sum_nat
case h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
i : ℕ
⊢ (∑' (i : ℕ), f i) - ∑ j in range i, f j = ∑' (k : ℕ), f (k + i)
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
⊢ (fun i => (∑' (i : ℕ), f i) - ∑ j in range i, f j) = fun i => ∑' (k : ℕ), f (k + i)
ext1 i
no goals
case h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : Summable f
i : ℕ
⊢ (∑' (i : ℕ), f i) - ∑ j in range i, f j = ∑' (k : ℕ), f (k + i)
rw [sub_eq_iff_eq_add, add_comm, sum_add_tsum_nat_add i hf]
case h.e'_3.h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
x✝ : ℕ
⊢ (∑' (k : ℕ), f (k + x✝)) = 0
case neg
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
convert tendsto_const_nhds (α := α) (β := ℕ) (a := 0) (f := atTop)
case h.e'_3.h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
i : ℕ
⊢ (∑' (k : ℕ), f (k + i)) = 0
case h.e'_3.h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
x✝ : ℕ
⊢ (∑' (k : ℕ), f (k + x✝)) = 0
rename_i i
case h.e'_3.h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
i : ℕ
hf : ¬Summable fun n => f (n + i)
⊢ (∑' (k : ℕ), f (k + i)) = 0
case h.e'_3.h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
hf : ¬Summable f
i : ℕ
⊢ (∑' (k : ℕ), f (k + i)) = 0
rw [← summable_nat_add_iff i] at hf
no goals
case h.e'_3.h
α : Type u_1
β : Type ?u.464802
γ : Type ?u.464805
δ : Type ?u.464808
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
f : ℕ → α
i : ℕ
hf : ¬Summable fun n => f (n + i)
⊢ (∑' (k : ℕ), f (k + i)) = 0
exact tsum_eq_zero_of_not_summable hf