awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun (N : ℕ) ↦ term_sum s N) atTop
    (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
have ha : Tendsto
  (fun (N : ℕ) ↦
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s))
  atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
Tactic: simp_rw [term_sum_of_lt _ hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto
    (fun (N : ℕ) ↦
      1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
        1 / s *
          (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s))
    atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
have ha : Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))
Tactic: apply Tendsto.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
ha : Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))
⊢ Tendsto
    (fun (N : ℕ) ↦
      1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
        1 / s *
          (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s))
    atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
have ha₁ : Tendsto
  (fun (x : ℕ) ↦
    1 / s *
      (∑ n ∈ Finset.range x, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s))
  atTop (𝓝 (1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
Tactic: apply Tendsto.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))
have ha : Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop
  (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
Tactic: rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop
    (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
have ha : Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) - 1 / (s - 1) * (1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop
  (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
Tactic: simp_rw [mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) - 1 / (s - 1) * (1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop
    (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
have ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1)) atTop (𝓝 0)
Tactic: refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ 0 < s - 1
have linarith : s - 1 ≤ 0 → 1 - s + (s - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1)) atTop (𝓝 0)
have ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) atTop atTop
Tactic: refine tendsto_const_nhds.div_atTop <| (tendsto_rpow_atTop (by linarith)).comp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto
    (fun (x : ℕ) ↦
      1 / s *
        (∑ n ∈ Finset.range x, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s))
    atTop (𝓝 (1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
have ha : Tendsto
  (fun (x : ℕ) ↦
    1 / s *
      (∑ n ∈ Finset.range x, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s))
  atTop (𝓝 (1 / s * HSub.hSub (α := ℝ) (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) 0))
Tactic: rw [← sub_zero (tsum _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto
    (fun (x : ℕ) ↦
      1 / s *
        (∑ n ∈ Finset.range x, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s))
    atTop (𝓝 (1 / s * HSub.hSub (α := ℝ) (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) 0))
have apply : Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ s
Tactic: apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
apply : Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ s
⊢ Tendsto
    (fun (x : ℕ) ↦
      1 / s *
        (∑ n ∈ Finset.range x, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s))
    atTop (𝓝 (1 / s * HSub.hSub (α := ℝ) (∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s) 0))
have apply₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)
Tactic: apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)
have hh : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)) atTop (𝓝 0)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
hh : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)
have hgf : LE.le (α := ℕ → ℝ) (fun (x : ℕ) ↦ 0) fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
hh : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)) atTop (𝓝 0)
hgf : LE.le (α := ℕ → ℝ) (fun (x : ℕ) ↦ 0) fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)
have hfh : LE.le (α := ℕ → ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) fun (n : ℕ) ↦
  HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
hh : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)) atTop (𝓝 0)
hgf : LE.le (α := ℕ → ℝ) (fun (x : ℕ) ↦ 0) fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s
hfh :
  LE.le (α := ℕ → ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)
have apply : ℕ → ℝ
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
have transitivity : (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s
Tactic: transitivity (n + 1) / (n + 1) ^ s
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
transitivity :
  (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s
⊢ (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
have transitivity₁ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
Tactic: transitivity (n + 1) / (n + 1) ^ s
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s
have hab : (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑n : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
have hab : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
have hab : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s
Tactic: rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
hab :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s =
    (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
have hab₁ : LE.le (α := ℝ) 0 (↑(n + 1) : ℝ)
Tactic: rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
hab :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s =
    (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s
hab₁ : LE.le (α := ℝ) 0 (↑(n + 1) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
have hab₂ : HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ≠ 0
Tactic: rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s =
    (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s
have hab : (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s = (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1) = 1 - s * term_tsum s
have rw : ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1) =
  1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: rw [term_tsum_of_lt hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1) =
    1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have generalize : ∀ (Z : ℝ), Z - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * Z)
Tactic: generalize (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) = Z
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ s - 1 ≠ 0
have linarith : s - 1 = 0 → 1 - s + (s - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
⊢ (↑(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 : ℕ
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ term (n + 1) x) (Ici 1)
have simp : ContinuousOn (Y := ℝ)
  (fun (x : ℝ) ↦
    @integral _ _ _ _ measurableSpace
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x_1 : ℝ) ↦
      (x_1 - (↑(n + 1) : ℝ)) / x_1 ^ (x + 1))
  (Ici 1)
Tactic: simp only [term, intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
⊢ ContinuousOn (Y := ℝ)
    (fun (x : ℝ) ↦
      @integral _ _ _ _ measurableSpace
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x_1 : ℝ) ↦
        (x_1 - (↑(n + 1) : ℝ)) / x_1 ^ (x + 1))
    (Ici 1)
have hF_meas : ∀ (x : ℝ),
  Membership.mem («γ» := Set ℝ) (Ici 1) x →
    AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (a : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1))
      (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
Tactic: apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hF_meas :
  ∀ (x : ℝ),
    Membership.mem («γ» := Set ℝ) (Ici 1) x →
      AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (a : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1))
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
⊢ ContinuousOn (Y := ℝ)
    (fun (x : ℝ) ↦
      @integral _ _ _ _ measurableSpace
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x_1 : ℝ) ↦
        (x_1 - (↑(n + 1) : ℝ)) / x_1 ^ (x + 1))
    (Ici 1)
have h_bound : ∀ (x : ℝ),
  Membership.mem («γ» := Set ℝ) (Ici 1) x →
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
      ‖(a - (↑(n + 1) : ℝ)) / a ^ (x + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
Tactic: apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hF_meas :
  ∀ (x : ℝ),
    Membership.mem («γ» := Set ℝ) (Ici 1) x →
      AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (a : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1))
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
h_bound :
  ∀ (x : ℝ),
    Membership.mem («γ» := Set ℝ) (Ici 1) x →
      ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
        ‖(a - (↑(n + 1) : ℝ)) / a ^ (x + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
⊢ ContinuousOn (Y := ℝ)
    (fun (x : ℝ) ↦
      @integral _ _ _ _ measurableSpace
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x_1 : ℝ) ↦
        (x_1 - (↑(n + 1) : ℝ)) / x_1 ^ (x + 1))
    (Ici 1)
have bound_integrable : @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2)
  (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
Tactic: apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hF_meas :
  ∀ (x : ℝ),
    Membership.mem («γ» := Set ℝ) (Ici 1) x →
      AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (a : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1))
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
h_bound :
  ∀ (x : ℝ),
    Membership.mem («γ» := Set ℝ) (Ici 1) x →
      ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
        ‖(a - (↑(n + 1) : ℝ)) / a ^ (x + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
bound_integrable :
  @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2)
    (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
⊢ ContinuousOn (Y := ℝ)
    (fun (x : ℝ) ↦
      @integral _ _ _ _ measurableSpace
        (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1))) fun (x_1 : ℝ) ↦
        (x_1 - (↑(n + 1) : ℝ)) / x_1 ^ (x + 1))
    (Ici 1)
have h_cont : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
  ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1)) (Ici 1)
Tactic: apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
⊢ Membership.mem («γ» := Set ℝ) (Ici 1) s →
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
      ‖(a - (↑(n + 1) : ℝ)) / a ^ (s + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
have h_bound : ∀ (hs : 1 ≤ s),
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ‖(a - (↑(n + 1) : ℝ)) / a ^ (s + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
Tactic: (hs : 1 ≤ s)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ‖(a - (↑(n + 1) : ℝ)) / a ^ (s + 1)‖ ≤ (a - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) a 2
have h_bound : ∀ᵐ (x : ℝ),
  x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
    ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2
Tactic: rw [ae_restrict_iff' measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
      ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2
have h_bound : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
  ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2
Tactic: filter_upwards with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ ‖(x - (↑(n + 1) : ℝ)) / x ^ (s + 1)‖ ≤ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2
have this : 1 < x
Tactic: have : 1 < x := lt_of_le_of_lt (by simp) hx.1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 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) : ℝ)) / HPow.hPow (β := ℝ) x 2
have h_bound : (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / x ^ (s + 1) ≤ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / HPow.hPow (β := ℝ) x 2
Tactic: rw [norm_of_nonneg (div_nonneg (sub_nonneg.mpr hx.1.le) (by positivity)), Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
⊢ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / x ^ (s + 1) ≤ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / HPow.hPow (β := ℝ) x 2
have h_bound : 0 ≤ x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
h_bound : 0 ≤ x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / x ^ (s + 1) ≤ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / HPow.hPow (β := ℝ) x 2
have h_bound₁ : 1 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
h_bound : 0 ≤ x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_bound₁ : 1 ≤ x
⊢ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / x ^ (s + 1) ≤ (x - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / HPow.hPow (β := ℝ) x 2
have h_bound₂ : 2 ≤ s + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
this : 1 < x
⊢ 2 ≤ s + 1
have linarith : s + 1 < 2 → 1 - s + (s + 1 - 2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2)
    (Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)))
have bound_integrable : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / HPow.hPow (β := ℝ) x 2) volume (↑(n + 1) : ℝ)
  (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
Tactic: rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
    ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (a - (↑(n + 1) : ℝ)) / a ^ (x + 1)) (Ici 1)
have h_cont : ∀ᵐ (x : ℝ),
  x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
    ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
Tactic: rw [ae_restrict_iff' measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) →
      ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
have h_cont : ∀ (x : ℝ) (hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)),
  ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
Tactic: filter_upwards with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
have h_cont : ∀ (s : ℝ) (hs : 1 ≤ s), ContinuousAt (Y := ℝ) (fun (x_1 : ℝ) ↦ x ^ (x_1 + 1)) s
Tactic: refine continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
h_cont : ∀ (s : ℝ) (hs : 1 ≤ s), ContinuousAt (Y := ℝ) (fun (x_1 : ℝ) ↦ x ^ (x_1 + 1)) s
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ (x - (↑(n + 1) : ℝ)) / x ^ (x_1 + 1)) (Ici 1)
have h_cont₁ : ∀ (s : ℝ) (hs : 1 ≤ s), x ^ (s + 1) ≠ 0
Tactic: refine continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < s + 1
have linarith : s + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - s) + (s + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1) : ℝ) (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1)
s : ℝ
hs : 1 ≤ s
linarith : s + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - s) + (s + 1 - 0) = 0
⊢ 0 < s + 1
have linarith₁ : s + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ ContinuousOn term_tsum (Ici 1)
have refine : ∀ (n : ℕ) (s : ℝ) (hs : Membership.mem («γ» := Set ℝ) (Ici 1) s), ‖term (n + 1) s‖ ≤ term (n + 1) 1
Tactic: refine continuousOn_tsum (fun i ↦ continuousOn_term _) term_tsum_one.summable (fun n s hs ↦ ?_)