-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- For `1 < s`, the topological sum of `ZetaAsymptotics.term (n + 1) s` over all `n : ℕ` is
`1 / (s - 1) - ζ s / s`.
-/
lemma term_tsum_of_lt {s : ℝ} (hs : 1 < s) :
    term_tsum s = (1 / (s - 1) - 1 / s * ∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s)

Proof state:
case ha.hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
rw [← sub_zero (tsum _)]

Result:
case ha.hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * (∑' (n : ℕ), 1 / (↑n + 1) ^ s - 0)))

Proof state:
case hfh
s : ℝ
hs : 1 < s
⊢ (fun k => ↑k / (↑k + 1) ^ s) ≤ fun n => (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
intro n

Result:
case hfh
s : ℝ
hs : 1 < s
n : ℕ
⊢ (fun k => ↑k / (↑k + 1) ^ s) n ≤ (fun n => (1 / ↑(n + 1)) ^ (s - 1)) n

Proof state:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun k => ↑k / (↑k + 1) ^ s) atTop (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds

Result:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto ?m.105177 atTop (𝓝 0)

case hgf
s : ℝ
hs : 1 < s
⊢ (fun x => 0) ≤ fun k => ↑k / (↑k + 1) ^ s

case hfh
s : ℝ
hs : 1 < s
⊢ (fun k => ↑k / (↑k + 1) ^ s) ≤ ?m.105177

s : ℝ
hs : 1 < s
⊢ ℕ → ℝ

Proof state:
case ha
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, term (i + 1) s) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
change Tendsto (fun N ↦ term_sum s N) atTop _

Result:
case ha
s : ℝ
hs : 1 < s
⊢ Tendsto (fun N => term_sum s N) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Proof state:
case ha
s : ℝ
hs : 1 < s
⊢ Tendsto
    (fun N =>
      1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s))
    atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
apply Tendsto.sub

Result:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))

case ha.hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Proof state:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 (0 ^ (s - 1)))

Tactic:
refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)

Result:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => 1 / ↑(n + 1)) atTop (𝓝 0)

Proof state:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun k => ↑k + 1) atTop atTop

Tactic:
exact tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop

Result:
no goals

Proof state:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto ?m.105177 atTop (𝓝 0)

Tactic:
change Tendsto (fun n : ℕ ↦ (1 / ↑(n + 1) : ℝ) ^ (s - 1)) ..

Result:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 0)

Proof state:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))

Tactic:
simp_rw [mul_sub, mul_one]

Result:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / (s - 1) - 1 / (s - 1) * (1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))

Proof state:
case ha
s : ℝ
hs : 1 < s
⊢ Tendsto (fun N => term_sum s N) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
simp_rw [term_sum_of_lt _ hs]

Result:
case ha
s : ℝ
hs : 1 < s
⊢ Tendsto
    (fun N =>
      1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s))
    atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Proof state:
s : ℝ
hs : 1 < s
⊢ s - 1 ≠ 0

Tactic:
linarith

Result:
no goals

Proof state:
s : ℝ
hs : 1 < s
⊢ 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0)

Tactic:
simp

Result:
no goals

Proof state:
case hfh
s : ℝ
hs : 1 < s
n : ℕ
⊢ (fun k => ↑k / (↑k + 1) ^ s) n ≤ (fun n => (1 / ↑(n + 1)) ^ (s - 1)) n

Tactic:
dsimp only

Result:
case hfh
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)

Proof state:
case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]

Result:
case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) / ↑(n + 1) ^ s

case hab.hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

case hab.hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Proof state:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / (s - 1) - 1 / (s - 1) * (1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))

Tactic:
refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)

Result:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun k => 1 / (↑k + 1) ^ (s - 1)) atTop (𝓝 0)

Proof state:
s : ℝ
hs : 1 < s
⊢ 0 < s - 1

Tactic:
linarith

Result:
no goals

Proof state:
case ha.hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * (∑' (n : ℕ), 1 / (↑n + 1) ^ s - 0)))

Tactic:
apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul

Result:
s : ℝ
hs : 1 < s
⊢ Summable fun i => 1 / (↑i + 1) ^ s

s : ℝ
hs : 1 < s
⊢ Tendsto (fun k => ↑k / (↑k + 1) ^ s) atTop (𝓝 0)

Proof state:
case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n ≤ ↑n + 1

Tactic:
linarith

Result:
no goals

Proof state:
case hfh
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
transitivity (n + 1) / (n + 1) ^ s

Result:
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (↑n + 1) / (↑n + 1) ^ s

s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)

Proof state:
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (↑n + 1) / (↑n + 1) ^ s

Tactic:
gcongr

Result:
case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n ≤ ↑n + 1

Proof state:
case hab.hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

case hab.hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
all_goals positivity

Result:
no goals

Proof state:
case hgf
s : ℝ
hs : 1 < s
n : ℕ
⊢ (fun x => 0) n ≤ (fun k => ↑k / (↑k + 1) ^ s) n

Tactic:
positivity

Result:
no goals

Proof state:
case hgf
s : ℝ
hs : 1 < s
⊢ (fun x => 0) ≤ fun k => ↑k / (↑k + 1) ^ s

Tactic:
intro n

Result:
case hgf
s : ℝ
hs : 1 < s
n : ℕ
⊢ (fun x => 0) n ≤ (fun k => ↑k / (↑k + 1) ^ s) n

Proof state:
case hab.hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
s : ℝ
hs : 1 < s
⊢ term_tsum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
apply HasSum.tsum_eq

Result:
case ha
s : ℝ
hs : 1 < s
⊢ HasSum (fun b => term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Proof state:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))

Tactic:
rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]

Result:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x => 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))

Proof state:
s : ℝ
hs : 1 < s
⊢ 0 ≤ s - 1

Tactic:
linarith

Result:
no goals

Proof state:
s : ℝ
hs : 1 < s
⊢ 𝓝 0 = 𝓝 (0 ^ (s - 1))

Tactic:
rw [zero_rpow]

Result:
s : ℝ
hs : 1 < s
⊢ s - 1 ≠ 0

Proof state:
s : ℝ
hs : 1 < s
⊢ Summable fun i => 1 / (↑i + 1) ^ s

Tactic:
exact_mod_cast (summable_nat_add_iff 1).mpr (summable_one_div_nat_rpow.mpr hs)

Result:
no goals

Proof state:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => 1 / ↑(n + 1)) atTop (𝓝 0)

Tactic:
exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)

Result:
no goals

Proof state:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun k => 1 / (↑k + 1) ^ (s - 1)) atTop (𝓝 0)

Tactic:
refine tendsto_const_nhds.div_atTop <| (tendsto_rpow_atTop (by linarith)).comp ?_

Result:
case ha.hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun k => ↑k + 1) atTop atTop