awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
rwa : (-s).re - re 1 + r < -1
rwa₁ : (-s).re - 1 + r < -1
rwa₂ : -s.re - 1 + r < -1
rwa₃ : -(1 + s.re) + r < -1
⊢ (-s - 1).re + r < -1
have rwa₄ : r < 1 + s.re + -1
Tactic: rwa [sub_re, one_re, neg_re, neg_sub_left, neg_add_lt_iff_lt_add, add_neg_cancel_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
have h₁ : (-s - 1).re + r < -1
Tactic: have h₁ : (-s - 1).re + r < -1 := by
    rwa [sub_re, one_re, neg_re, neg_sub_left, neg_add_lt_iff_lt_add, add_neg_cancel_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
have h₂ : s ≠ 0
Tactic: have h₂ : s ≠ 0 := ne_zero_of_re_pos (hr.trans_lt hs)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
have h₃ : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
  DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
Tactic: have h₃ (t : ℝ) (ht : t ∈ Set.Ici 1) : DifferentiableAt ℝ (fun x : ℝ ↦ (x : ℂ) ^ (-s)) t :=
    differentiableAt_id.ofReal_cpow_const (zero_lt_one.trans_le ht).ne' (neg_ne_zero.mpr h₂)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
n : ℕ
⊢ Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
have rw : Eq (α := ℂ) (∑ k ∈ insert 0 (Icc (HAdd.hAdd (α := ℕ) 0 1) n), f k) (∑ k ∈ Icc 1 n, f k)
Tactic: rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
n : ℕ
rw : Eq (α := ℂ) (∑ k ∈ insert 0 (Icc (HAdd.hAdd (α := ℕ) 0 1) n), f k) (∑ k ∈ Icc 1 n, f k)
⊢ Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
have rw₁ : f 0 + ∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x = ∑ k ∈ Icc 1 n, f k
Tactic: rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
n : ℕ
rw : Eq (α := ℂ) (∑ k ∈ insert 0 (Icc (HAdd.hAdd (α := ℕ) 0 1) n), f k) (∑ k ∈ Icc 1 n, f k)
rw₁ : f 0 + ∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x = ∑ k ∈ Icc 1 n, f k
⊢ Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
have rw₂ : HAdd.hAdd (α := ℂ) 0 (∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x) = ∑ k ∈ Icc 1 n, f k
Tactic: rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
n : ℕ
rw : Eq (α := ℂ) (∑ k ∈ insert 0 (Icc (HAdd.hAdd (α := ℕ) 0 1) n), f k) (∑ k ∈ Icc 1 n, f k)
rw₁ : f 0 + ∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x = ∑ k ∈ Icc 1 n, f k
rw₂ : HAdd.hAdd (α := ℂ) 0 (∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x) = ∑ k ∈ Icc 1 n, f k
⊢ Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
have rw₃ : Eq (α := ℂ) (∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x) (∑ k ∈ Icc 1 n, f k)
Tactic: rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
n : ℕ
rw : Eq (α := ℂ) (∑ k ∈ insert 0 (Icc (HAdd.hAdd (α := ℕ) 0 1) n), f k) (∑ k ∈ Icc 1 n, f k)
rw₁ : f 0 + ∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x = ∑ k ∈ Icc 1 n, f k
rw₂ : HAdd.hAdd (α := ℂ) 0 (∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x) = ∑ k ∈ Icc 1 n, f k
rw₃ : Eq (α := ℂ) (∑ x ∈ Icc (HAdd.hAdd (α := ℕ) 0 1) n, f x) (∑ k ∈ Icc 1 n, f k)
⊢ Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
have rw₄ : Eq (α := ℂ) (∑ x ∈ Icc 1 n, f x) (∑ k ∈ Icc 1 n, f k)
Tactic: rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
have h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
Tactic: have h₄ : ∀ n, ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k := fun n ↦ by
    rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
have hO₁ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
Tactic: simp_rw [← h₄] at hO
Cleared hypotheses: hO
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
have rw : LSeries f s =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
    s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))
Tactic: rw [← integral_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ LSeries f s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))
have refine : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ i ∈ range (n + 1), LSeries.term f s i) atTop
  (𝓝
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
Tactic: refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).mpr hS.hasSum.tendsto_sum_nat) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ i ∈ range (n + 1), LSeries.term f s i) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
        s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
have simp_rw : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ x ∈ Icc 0 n, HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x) atTop
  (𝓝
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
Tactic: simp_rw [Nat.range_succ_eq_Icc_zero, LSeries.term_def₀ hf, mul_comm (f _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ x ∈ Icc 0 n, HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
        s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
have h : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
    s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))) =
  HSub.hSub (α := ℂ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k))
Tactic: convert!
    tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))) =
    HSub.hSub (α := ℂ) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ x ∈ Icc 0 n, HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
        s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
have convert_1 : LocallyIntegrableOn (X := ℝ) (ε := ℂ) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (Set.Ici 1) volume
Tactic: convert!
    tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))) =
    HSub.hSub (α := ℂ) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k))
convert_1 : LocallyIntegrableOn (X := ℝ) (ε := ℂ) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (Set.Ici 1) volume
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ x ∈ Icc 0 n, HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
        s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
have convert_2 : Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
  atTop (𝓝 0)
Tactic: convert!
    tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))) =
    HSub.hSub (α := ℂ) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k))
convert_1 : LocallyIntegrableOn (X := ℝ) (ε := ℂ) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (Set.Ici 1) volume
convert_2 :
  Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
    atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ x ∈ Icc 0 n, HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
        s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))))
have convert_3 : IsBigO (E := ℂ) (F := ℝ) atTop
  (fun (t : ℝ) ↦ HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k)) fun (x : ℝ) ↦
  x ^ ((-s - 1).re + r)
Tactic: convert!
    tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1)))) =
    HSub.hSub (α := ℂ) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k))
have h : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
    s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1))))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
    -HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) a) (∑ k ∈ Icc 0 ⌊a⌋₊, f k))
Tactic: rw [zero_sub, ← integral_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(s + 1))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      -HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) a) (∑ k ∈ Icc 0 ⌊a⌋₊, f k))
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ioi 1) t),
  s * ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))) =
    -HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Ioi 1) t
⊢ s * ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))) =
    -HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k)
have h : s * ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))) = -(-s * (↑t : ℂ) ^ (-s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k)
Tactic: rw [deriv_ofReal_cpow_const (zero_lt_one.trans ht).ne', h₄]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Ioi 1) t
h : s * ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))) = -(-s * (↑t : ℂ) ^ (-s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k)
⊢ s * ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))) =
    -HMul.hMul (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t) (∑ k ∈ Icc 0 ⌊t⌋₊, f k)
have h₅ : -s ≠ 0
Tactic: rw [deriv_ofReal_cpow_const (zero_lt_one.trans ht).ne', h₄]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
    atTop (𝓝 0)
have hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)
Tactic: have hlim : Tendsto (fun n : ℕ ↦ (n : ℝ) ^ (-(s.re - r))) atTop (𝓝 0) :=
      (tendsto_rpow_neg_atTop (by rwa [sub_pos])).comp tendsto_natCast_atTop_atTop
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) t
h₄ : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 0 n, f k) (∑ k ∈ Icc 1 n, f k)
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
    atTop (𝓝 0)
have convert_2 : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re)
Tactic: refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow (-s.re) _ _ ?_ hO ?_).trans_tendsto hlim