awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ ‖term (n + 1) s‖ ≤ term (n + 1) 1
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
  (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
Tactic: rw [term, term, norm_of_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
rw :
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1,
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
⊢ ‖term (n + 1) s‖ ≤ term (n + 1) 1
have rw₁ : LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
Tactic: rw [term, term, norm_of_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ (↑(n + 1) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 < (↑(n + 1) : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 - (↑(n + 1) : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1,
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
have simp_rw : LE.le (α := ℝ)
  (@integral _ _ _ _ measurableSpace
    (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
    (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
  (@integral _ _ _ _ measurableSpace
    (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
    (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
Tactic: simp_rw [intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
have refine_1 : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
  (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
refine_1 :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
have refine_2 : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
  (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
refine_1 :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
refine_2 :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
    (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)) volume
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
have refine_3 : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
  (x - (↑(n + 1) : ℝ)) / x ^ (s + 1) ≤ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1) ≤ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1
have this : 1 ≤ x
Tactic: have : 1 ≤ x := le_trans (by simp) hx.1.le
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
⊢ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1) ≤ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1
have refine_3 : 0 ≤ x - (↑(n + 1) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 ≤ x
refine_3 : 0 ≤ x - (↑(n + 1) : ℝ)
⊢ (x - (↑(n + 1) : ℝ)) / x ^ (s + 1) ≤ (x - (↑(n + 1) : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1
have refine_3₁ : 1 ≤ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ LE.le (α := ℝ) 0
    (∫ (x : ℝ) in (↑(n + 1) : ℝ)..HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1, (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
have rw : LE.le (α := ℝ) 0
  (@integral _ _ _ _ measurableSpace
    (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
    (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
Tactic: rw [intervalIntegral.integral_of_le (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
have refine_1 : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)), 0 ≤ x - (↑(n + 1) : ℝ)
Tactic: refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ div_nonneg ?_ (rpow_nonneg ?_ _))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
refine_1 : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)), 0 ≤ x - (↑(n + 1) : ℝ)
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x : ℝ) ↦
      (x - (↑(n + 1) : ℝ)) / x ^ (s + 1))
have refine_2 : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)), 0 ≤ x
Tactic: refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ div_nonneg ?_ (rpow_nonneg ?_ _))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ 0 ≤ x - (↑(n + 1) : ℝ)
have linarith : x - (↑(n + 1) : ℝ) < 0 → x - (↑(n + 1) : ℝ) - 0 + ((↑(n + 1) : ℝ) - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ 0 ≤ x
have linarith : x < 0 → HSub.hSub (α := ℝ) 0 (↑(n + 1) : ℝ) + (x - 0) + ((↑(n + 1) : ℝ) - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ Tendsto (fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)) (𝓝[>] 1) (𝓝 (↑γ : ℂ))
have apply : (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1]
  fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)
Tactic: apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1]
    fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)
have h : ∀ (s : ℝ) (hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s),
  (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) s =
    riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)
Tactic: filter_upwards [self_mem_nhdsWithin] with s hs
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
⊢ (Complex.ofReal ∘ fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) s =
    riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)
have h : ∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ) = riemannZeta (↑s : ℂ)
Tactic: simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
      Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
⊢ ∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ) = riemannZeta (↑s : ℂ)
have h : Eq (α := ℂ) (∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ))
  (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ))
Tactic: rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
⊢ Eq (α := ℂ) (∑' (a : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ s) : ℂ))
    (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ))
have h : ∀ (n : ℕ), 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)
Tactic: congr 1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
n : ℕ
⊢ 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)
have h : 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑s : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)
Tactic: rw [Complex.ofReal_cpow (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
n : ℕ
⊢ 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑s : ℂ) = 1 / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑s : ℂ)
have h : 1 / HPow.hPow (α := ℂ) (↑(n + 1) : ℂ) (↑s : ℂ) = 1 / HPow.hPow (α := ℂ) (↑(n + 1) : ℂ) (↑s : ℂ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (s : ℝ) ↦ riemannZeta (↑s : ℂ) - 1 / ((↑s : ℂ) - 1)) (𝓝[>] 1) (𝓝 (↑γ : ℂ))
have suffices : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
aux2 :
  Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
have this : ∑' (b : ℕ), term (b + 1) 1 = 1 - γ
Tactic: have := term_tsum_one.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
aux2 :
  Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : ∑' (b : ℕ), term (b + 1) 1 = 1 - γ
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
have this₁ : γ = 1 - term_tsum 1
Tactic: rw [← term_tsum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
have suffices : Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
have hl : EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
  ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
Tactic: apply Tendsto.congr'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
hl :
  EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
    ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
have h : Tendsto (fun (s : ℝ) ↦ 1 - s * term_tsum s) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
Tactic: apply Tendsto.congr'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
hl :
  EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
    ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
h : Tendsto (fun (s : ℝ) ↦ 1 - s * term_tsum s) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
have f₁ : ℝ → ℝ
Tactic: apply Tendsto.congr'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
    ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
have h : ∀ (a : ℝ),
  Membership.mem («γ» := Set ℝ)
    {x : ℝ |
      Membership.mem («γ» := Set ℝ) (Ioi 1) x →
        Membership.mem («γ» := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                1 - x * term_tsum x = (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) x)
              x}
          x}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h :
  ∀ (a : ℝ),
    Membership.mem («γ» := Set ℝ)
      {x : ℝ |
        Membership.mem («γ» := Set ℝ) (Ioi 1) x →
          Membership.mem («γ» := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  1 - x * term_tsum x =
                    (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) x)
                x}
            x}
      a
⊢ EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
    ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
have h₁ : ∀ (a : ℝ),
  Membership.mem («γ» := Set ℝ) (Ioi 1) a →
    1 - a * term_tsum a = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ a - 1 / (a - 1)
Tactic: filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (s : ℝ) ↦ 1 - s * term_tsum s) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
have h : Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (term_tsum 1))
Tactic: apply tendsto_const_nhds.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (term_tsum 1))
have h : Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (1 * term_tsum 1))
Tactic: rw [← one_mul (term_tsum 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (1 * term_tsum 1))
have h : Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))
Tactic: apply (tendsto_id.mono_left nhdsWithin_le_nhds).mul
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))
have this : ContinuousWithinAt term_tsum (Ici 1) 1
Tactic: have := continuousOn_term_tsum.continuousWithinAt self_mem_Ici
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
this : ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))
have obtain : ∀ (C : ℂ) (hC : Tendsto f (𝓝[≠] 1) (𝓝 C)), Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))
Tactic: obtain ⟨C, hC⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))
have suffices : Tendsto (fun (s : ℝ) ↦ f (↑s : ℂ)) (𝓝[>] 1) (𝓝 C)
Tactic: suffices Tendsto (fun s : ℝ ↦ f s) _ _
      from (tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_nhds_right) ▸ hC
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun (s : ℝ) ↦ f (↑s : ℂ)) (𝓝[>] 1) (𝓝 C)
have refine_1 : Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)
Tactic: refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
refine_1 : Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)
⊢ Tendsto (fun (s : ℝ) ↦ f (↑s : ℂ)) (𝓝[>] 1) (𝓝 C)
have refine_2 : ∀ᶠ (x : ℝ) in 𝓝[>] 1, Membership.mem («γ» := Set ℂ) {1}ᶜ (↑x : ℂ)
Tactic: refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 1, Membership.mem («γ» := Set ℂ) {1}ᶜ (↑x : ℂ)
have h : ∀ (a : ℝ) (ha : Membership.mem («γ» := Set ℝ) (Ioi 1) a), Membership.mem («γ» := Set ℂ) {1}ᶜ (↑a : ℂ)
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : Membership.mem («γ» := Set ℝ) (Ioi 1) a
⊢ Membership.mem («γ» := Set ℂ) {1}ᶜ (↑a : ℂ)
have h : ¬a = 1
Tactic: rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))
have suffices : ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)
Tactic: suffices ∃ C, Tendsto f (𝓝[≠] 1) (𝓝 C) by
    obtain ⟨C, hC⟩ := this
    suffices Tendsto (fun s : ℝ ↦ f s) _ _
      from (tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_nhds_right) ▸ hC
    refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)
    · exact (Complex.continuous_ofReal.tendsto 1).mono_left (nhdsWithin_le_nhds ..)
    · filter_upwards [self_mem_nhdsWithin] with a ha
      rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]
      exact ne_of_gt ha
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)
have refine_1 : ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z
Tactic: refine ⟨_, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO ?_ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_1 : ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z
⊢ ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)
have refine_2 : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 1) (fun (z : ℂ) ↦ f z - f 1) fun (z : ℂ) ↦ (z - 1)⁻¹
Tactic: refine ⟨_, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO ?_ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z
have h : ∀ (s : ℂ) (hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s), DifferentiableAt ℂ f s
Tactic: filter_upwards [self_mem_nhdsWithin] with s hs
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
⊢ DifferentiableAt ℂ f s
have h : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ s - 1) s
Tactic: refine (differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
h : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ s - 1) s
⊢ DifferentiableAt ℂ f s
have h₁ : s - 1 ≠ 0
Tactic: refine (differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
⊢ s - 1 ≠ 0
have h : ∀ (hs : s ≠ 1), s - 1 ≠ 0
Tactic: rwa [mem_compl_singleton_iff, ← sub_ne_zero] at hs
Cleared hypotheses: hs