Theorem: finsetSum_tendsto_tsum (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
have := Summable.hasSum_iff_tendsto_nat hf (m := ∑' (n : ℕ), f n) |>.mp hf.hasSum
State after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
have const := @tendsto_const_nhds (x := ∑ i in Finset.range N, f i) ℕ _ atTop
State after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
have := Filter.Tendsto.sub this const
State after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this :
  Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop
    (𝓝 (∑' (n : ℕ), f n - ∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this :
  Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop
    (𝓝 (∑' (n : ℕ), f n - ∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
rw [tsum_eq_partial_add_tail f hf (N := N), add_comm, add_sub_cancel_right] at this
State after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
apply this.congr'
State after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) =ᶠ[atTop] fun k => ∑ n ∈ Finset.Ico N k, f n

State before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) =ᶠ[atTop] fun k => ∑ n ∈ Finset.Ico N k, f n
Tactic:
filter_upwards [Filter.mem_atTop (N + 1)]
State after:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ ∀ (a : ℕ), N + 1 ≤ a → ∑ i ∈ Finset.range a, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N a, f n

State before:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ ∀ (a : ℕ), N + 1 ≤ a → ∑ i ∈ Finset.range a, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N a, f n
Tactic:
intro M hM
State after:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ ∑ i ∈ Finset.range M, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N M, f n

State before:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ ∑ i ∈ Finset.range M, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N M, f n
Tactic:
rw [Finset.sum_Ico_eq_sub]
State after:
case h.h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ N ≤ M

State before:
case h.h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ N ≤ M
Tactic:
linarith
State after:
no goals