Theorem: ZetaSum_aux3 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
let f := fun (n : ℕ) ↦ 1 / (n : ℂ) ^ s
State after:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))

State before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
have hf := Summable_rpow s_re_gt
State after:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))

State before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
simp_rw [Finset.Ioc_eq_Ico]
State after:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))

State before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
convert finsetSum_tendsto_tsum (f := fun n ↦ f (n + 1)) (N := N) ?_ using 1
State after:
case h.e'_3
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) = fun k => ∑ n ∈ Finset.Ico N k, f (n + 1)

case h.e'_5
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ 𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s) = 𝓝 (∑' (n : ℕ), f (n + N + 1))

N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Summable fun n => f (n + 1)

State before:
case h.e'_3
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) = fun k => ∑ n ∈ Finset.Ico N k, f (n + 1)
Tactic:
ext k
State after:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ n ∈ Finset.Ico N k, f (n + 1)

State before:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ n ∈ Finset.Ico N k, f (n + 1)
Tactic:
simp only [f]
State after:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ x ∈ Finset.Ico N k, 1 / ↑(x + 1) ^ s

State before:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ x ∈ Finset.Ico N k, 1 / ↑(x + 1) ^ s
Tactic:
convert Finset.sum_map (e := addRightEmbedding 1) ?_  ?_ using 2
State after:
case h.e'_2.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ Finset.Ico (N + 1) (k + 1) = Finset.map (addRightEmbedding 1) (Finset.Ico N k)

State before:
case h.e'_2.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ Finset.Ico (N + 1) (k + 1) = Finset.map (addRightEmbedding 1) (Finset.Ico N k)
Tactic:
ext n
State after:
case h.e'_2.h.a
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k n : ℕ
⊢ n ∈ Finset.Ico (N + 1) (k + 1) ↔ n ∈ Finset.map (addRightEmbedding 1) (Finset.Ico N k)

State before:
case h.e'_2.h.a
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k n : ℕ
⊢ n ∈ Finset.Ico (N + 1) (k + 1) ↔ n ∈ Finset.map (addRightEmbedding 1) (Finset.Ico N k)
Tactic:
simp only [Finset.mem_Ico, Finset.map_add_right_Ico]
State after:
no goals

State before:
case h.e'_5
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ 𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s) = 𝓝 (∑' (n : ℕ), f (n + N + 1))
Tactic:
congr
State after:
case h.e'_5.e_x.e_f
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun n => 1 / (↑n + ↑N + 1) ^ s) = fun n => f (n + N + 1)

State before:
case h.e'_5.e_x.e_f
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun n => 1 / (↑n + ↑N + 1) ^ s) = fun n => f (n + N + 1)
Tactic:
ext n
State after:
case h.e'_5.e_x.e_f.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
n : ℕ
⊢ 1 / (↑n + ↑N + 1) ^ s = f (n + N + 1)

State before:
case h.e'_5.e_x.e_f.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
n : ℕ
⊢ 1 / (↑n + ↑N + 1) ^ s = f (n + N + 1)
Tactic:
simp only [one_div, Nat.cast_add, Nat.cast_one, f]
State after:
no goals

State before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Summable fun n => f (n + 1)
Tactic:
rwa [summable_nat_add_iff (k := 1)]
State after:
no goals