-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- First version of the limit formula, with a limit over real numbers tending to 1 from above. -/
lemma tendsto_riemannZeta_sub_one_div_nhds_right :
    Tendsto (fun s : ℝ ↦ riemannZeta s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Proof state:
aux2 : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : ∑' (b : ℕ), term (b + 1) 1 = 1 - γ
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
rw [← term_tsum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this

Result:
aux2 : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : γ = 1 - term_tsum 1
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Proof state:
aux2 : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
have := term_tsum_one.tsum_eq

Result:
aux2 : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : ∑' (b : ℕ), term (b + 1) 1 = 1 - γ
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Proof state:
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ Tendsto (fun s => riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)

Tactic:
apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'

Result:
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ (Complex.ofReal ∘ fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1] fun s =>
    riemannZeta ↑s - 1 / (↑s - 1)

Proof state:
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ 1 < (↑s).re

Tactic:
simpa using hs

Result:
no goals

Proof state:
case h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = riemannZeta ↑s

Tactic:
rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]

Result:
case h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑s

Proof state:
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
suffices aux2 : Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
  (𝓝[>] 1) (𝓝 (1 - term_tsum 1)) by
  have := term_tsum_one.tsum_eq
  rw [← term_tsum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this
  simpa only [this] using aux2

Result:
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))

Proof state:
case h

⊢ Tendsto (fun x => x * term_tsum x) (𝓝[>] 1) (𝓝 (1 * term_tsum 1))

Tactic:
apply (tendsto_id.mono_left nhdsWithin_le_nhds).mul

Result:
case h

⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))

Proof state:
case h

⊢ Tendsto (fun s => 1 - s * term_tsum s) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))

Tactic:
apply tendsto_const_nhds.sub

Result:
case h

⊢ Tendsto (fun x => x * term_tsum x) (𝓝[>] 1) (𝓝 (term_tsum 1))

Proof state:
case hl

⊢ ?f₁ =ᶠ[𝓝[>] 1] fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm

Result:
no goals

Proof state:
case h

⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))

Tactic:
have := continuousOn_term_tsum.continuousWithinAt left_mem_Ici

Result:
case h
this : ContinuousWithinAt term_tsum (Ici 1) 1
⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))

Proof state:
⊢ Tendsto (fun s => riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)

Tactic:
suffices Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
  (𝓝[>] 1) (𝓝 γ) by
  apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'
  filter_upwards [self_mem_nhdsWithin] with s hs
  simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
    Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]
  rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]
  congr 1 with n
  rw [Complex.ofReal_cpow (by positivity)]
  norm_cast

Result:
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Proof state:
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ (Complex.ofReal ∘ fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1] fun s =>
    riemannZeta ↑s - 1 / (↑s - 1)

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs

Result:
case h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ (Complex.ofReal ∘ fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) s = riemannZeta ↑s - 1 / (↑s - 1)

Proof state:
case h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ (Complex.ofReal ∘ fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) s = riemannZeta ↑s - 1 / (↑s - 1)

Tactic:
simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
  Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]

Result:
case h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = riemannZeta ↑s

Proof state:
case h
this : ContinuousWithinAt term_tsum (Ici 1) 1
⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))

Tactic:
exact Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)

Result:
no goals

Proof state:
aux2 : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : γ = 1 - term_tsum 1
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
simpa only [this] using aux2

Result:
no goals

Proof state:
case h.e_f.h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑(↑n + 1) ^ ↑s = 1 / (↑n + 1) ^ ↑s

Tactic:
norm_cast

Result:
no goals

Proof state:
case h

⊢ Tendsto (fun x => x * term_tsum x) (𝓝[>] 1) (𝓝 (term_tsum 1))

Tactic:
rw [← one_mul (term_tsum 1)]

Result:
case h

⊢ Tendsto (fun x => x * term_tsum x) (𝓝[>] 1) (𝓝 (1 * term_tsum 1))

Proof state:
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 0 ≤ ↑n + 1

Tactic:
positivity

Result:
no goals

Proof state:
case h.e_f.h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑((↑n + 1) ^ s) = 1 / (↑n + 1) ^ ↑s

Tactic:
rw [Complex.ofReal_cpow (by positivity)]

Result:
case h.e_f.h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑(↑n + 1) ^ ↑s = 1 / (↑n + 1) ^ ↑s

Proof state:
case h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑s

Tactic:
congr 1 with n

Result:
case h.e_f.h
this : Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑((↑n + 1) ^ s) = 1 / (↑n + 1) ^ ↑s

Proof state:
⊢ Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))

Tactic:
apply Tendsto.congr'

Result:
case hl

⊢ ?f₁ =ᶠ[𝓝[>] 1] fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)

case h

⊢ Tendsto ?f₁ (𝓝[>] 1) (𝓝 (1 - term_tsum 1))

case f₁

⊢ ℝ → ℝ