awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range 0,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ (s - 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
e_a :
  1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) +
      1 / (s - 1) * (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1) - 1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) ^ (s - 1))
⊢ ∑ x ∈ Finset.range (N + 1),
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ (s - 1))

Tactic:
rw [Finset.sum_range_succ, hN, Nat.cast_add_one]

Premises used: Nat.cast_add_one, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
⊢ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) +
      1 / (s - 1) * (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1) - 1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) ^ (s - 1))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ x ∈ Finset.range 0,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ (s - 1))
e_a₁ :
  ∀ (N : ℕ)
    (hN :
      ∑ x ∈ Finset.range N,
          1 / (s - 1) *
            (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
        1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))),
    ∑ x ∈ Finset.range (N + 1),
        1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
      1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ (s - 1))
⊢ ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))

Tactic:
induction N with
    | zero => simp
    | succ N hN =>
      rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf

Premises used: Nat.cast_add_one, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  (∑ i ∈ Finset.range N,
        (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ)) *
      s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) * s⁻¹
⊢ ∑ x ∈ Finset.range N,
      (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)

Tactic:
simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]

Premises used: mul_div_assoc, HDiv.hDiv, div_eq_mul_inv, mul_comm, mul_one, Finset.sum_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
⊢ (∑ i ∈ Finset.range N,
        (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ)) *
      s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) * s⁻¹

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ ∑ i ∈ Finset.range 0,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range 0, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑0 : ℝ) / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ s

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
e_a :
  ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
      (-((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
        (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
          HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
      (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s +
        -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s))
⊢ ∑ i ∈ Finset.range (N + 1),
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range (N + 1), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s -
      (↑(N + 1) : ℝ) / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ s

Tactic:
simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]

Premises used: add_assoc, sub_eq_add_neg, Nat.cast_add_one, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
e_a :
  -((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
      (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
        HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 =
    1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)
⊢ ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
      (-((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
        (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
          HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
      (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s +
        -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
⊢ -((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
      (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
        HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 =
    1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ i ∈ Finset.range 0,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range 0, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑0 : ℝ) / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ s
e_a₁ :
  ∀ (N : ℕ)
    (hN :
      ∑ i ∈ Finset.range N,
          (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
        ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s),
    ∑ i ∈ Finset.range (N + 1),
        (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
      ∑ n ∈ Finset.range (N + 1), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s -
        (↑(N + 1) : ℝ) / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ s
⊢ ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s

Tactic:
induction N with
    | zero => simp
    | succ N hN =>
      simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
      congr 1
      ring_nf

Premises used: add_assoc, sub_eq_add_neg, Nat.cast_add_one, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
ha : HasSum (fun (b : ℕ) ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
⊢ term_tsum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s

Tactic:
apply HasSum.tsum_eq

Premises used: HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
ha :
  Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, term (i + 1) s) atTop
    (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
⊢ HasSum (fun (b : ℕ) ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)

Tactic:
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)]

Premises used: HAdd.hAdd, ZetaAsymptotics.term_nonneg, OfNat.ofNat, hasSum_iff_tendsto_nat_of_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
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))
⊢ Tendsto (fun (N : ℕ) ↦ term_sum s N) atTop
    (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))

Tactic:
simp_rw [term_sum_of_lt _ hs]

Premises used: ZetaAsymptotics.term_sum_of_lt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
ha : Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))
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))
⊢ 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:
apply Tendsto.sub

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
ha :
  Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop
    (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
⊢ Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))

Tactic:
rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
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))
⊢ Tendsto (fun (x : ℕ) ↦ 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1))) atTop
    (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))

Tactic:
simp_rw [mul_sub, mul_one]

Premises used: mul_sub, mul_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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))

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

Premises used: tendsto_const_nhds, Filter.Tendsto.const_mul, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1)) atTop (𝓝 0)
⊢ 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:
refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)

Premises used: tendsto_const_nhds, Filter.Tendsto.const_mul, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
linarith : s - 1 ≤ 0 → 1 - s + (s - 1 - 0) = 0
⊢ 0 < s - 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
ha : Tendsto (β := ℝ) (fun (x : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ (s - 1)) atTop (𝓝 0)

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

Premises used: Filter.Tendsto.div_atTop, tendsto_const_nhds, tendsto_rpow_atTop, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) atTop atTop

Tactic:
tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop

Premises used: Filter.tendsto_atTop_add_const_right, tendsto_natCast_atTop_atTop
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) atTop atTop

Tactic:
exact tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop

Premises used: Filter.tendsto_atTop_add_const_right, tendsto_natCast_atTop_atTop
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
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))
⊢ 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:
rw [← sub_zero (tsum _)]

Premises used: sub_zero, tsum, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
apply : Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ s
apply₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)
⊢ 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:
apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul

Premises used: HasSum.tendsto_sum_nat, Filter.Tendsto.const_mul, Summable.hasSum, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ s

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

Premises used: Iff.mpr, summable_nat_add_iff, Real.summable_one_div_nat_rpow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
apply : ℕ → ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) atTop (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)) atTop (𝓝 0)

Tactic:
exact ((tendsto_const_div_atTop_nhds_zero_nat _).comp
          (tendsto_add_atTop_nat _)).rpow_const_nhds_zero (by linarith)

Premises used: tendsto_const_div_atTop_nhds_zero_nat, Filter.Tendsto.rpow_const_nhds_zero, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ LE.le (α := (fun (a : ℕ) ↦ ℝ) n) ((fun (x : ℕ) ↦ (0 : ℝ)) n)
    ((fun (x : ℕ) ↦ (↑x : ℝ) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 ^ s) n)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
transitivity :
  (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s
transitivity₁ :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
⊢ (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)

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

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
hab : (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (↑n : ℝ) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑n : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ)) = 0
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
hab : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s ≤ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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) : ℝ)
hab₂ : HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ≠ 0
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s = HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ^ (s - 1)

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

Premises used: Real.inv_rpow, div_mul, div_eq_mul_inv, Real.rpow_sub_one, one_div, mul_comm, div_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
hab hab₁ hab₂ hab₃ :
  (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s = (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s =
    (↑(n + 1) : ℝ) / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑(n + 1) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
n : ℕ
⊢ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
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)
⊢ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1) = 1 - s * term_tsum s

Tactic:
rw [term_tsum_of_lt hs]

Premises used: ZetaAsymptotics.term_tsum_of_lt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
generalize : ∀ (Z : ℝ), Z - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * Z)
⊢ ∑' (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:
generalize (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) = Z

Premises used: HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, tsum, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
Z : ℝ
linarith : s - 1 = 0 → 1 - s + (s - 1 - 0) = 0
⊢ s - 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : 1 < s
Z : ℝ
⊢ Z - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * Z)

Tactic:
field [(show s - 1 ≠ 0 by linarith)]
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
linarith :
  HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 < (↑(n + 1) : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 - (↑(n + 1) : ℝ)) = 0
⊢ (↑(n + 1) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
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)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ term (n + 1) x) (Ici 1)

Tactic:
simp only [term, intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]

Premises used: intervalIntegral.integral_of_le, ZetaAsymptotics.term
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)))
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)
⊢ 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:
apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))

Premises used: MeasureTheory.continuousOn_of_dominated
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ici 1) s
⊢ 0 < n + 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
⊢ ∀ (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:
exact fun s hs ↦ (term_welldef (by simp) (zero_lt_one.trans_le hs)).1.1

Premises used: zero_lt_one, And.left, LT.lt.trans_le, ZetaAsymptotics.term_welldef