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
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)
convert_2 :
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
    atTop (𝓝 0)
have convert_2₁ : -s.re + r ≤ -(s.re - r)
Tactic: refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow (-s.re) _ _ ?_ hO ?_).trans_tendsto hlim
-- 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)
⊢ -s.re + r ≤ -(s.re - r)
have linarith : -(s.re - r) < -s.re + r → -(s.re - r) - (-s.re + r) = 0
Tactic: linarith
-- 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
⊢ -(s + 1).re + r ≤ (-s - 1).re + r
have rw : (-(s + 1)).re + r ≤ (-s - 1).re + r
Tactic: rw [← neg_re, neg_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
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
rw : (-(s + 1)).re + r ≤ (-s - 1).re + r
⊢ -(s + 1).re + r ≤ (-s - 1).re + r
have rw₁ : (-s - 1).re + r ≤ (-s - 1).re + r
Tactic: rw [← neg_re, neg_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
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
⊢ 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)
have convert_3 : IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) fun (t : ℝ) ↦ t ^ (-(s + 1).re)
Tactic: refine .mul_atTop_rpow_of_isBigO_rpow (-(s + 1).re) r _ ?_ ?_ (by rw [← neg_re, neg_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
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
convert_3 : IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) fun (t : ℝ) ↦ t ^ (-(s + 1).re)
⊢ 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)
have convert_3₁ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 0 ⌊t⌋₊, f k) fun (t : ℝ) ↦ t ^ r
Tactic: refine .mul_atTop_rpow_of_isBigO_rpow (-(s + 1).re) r _ ?_ ?_ (by rw [← neg_re, neg_add'])
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
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
⊢ (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ (fun (n : ℕ) ↦ if n = 0 then 0 else f n) x = f x) x} x}
    a
Tactic: filter_upwards [eventually_ne_atTop 0] with n h using if_neg h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
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 :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ (fun (n : ℕ) ↦ if n = 0 then 0 else f n) x = f x) x} x}
      a
⊢ (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f
have h₁ : ∀ (a : ℕ), a ≠ 0 → (if a = 0 then 0 else f a) = f a
Tactic: filter_upwards [eventually_ne_atTop 0] with n h using if_neg h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
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 hS₁ : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) s
Tactic: rw [← LSeriesSummable_congr' s (f := fun n ↦ if n = 0 then 0 else f n)
    (by filter_upwards [eventually_ne_atTop 0] with n h using if_neg h)] at hS
Cleared hypotheses: hS, hO
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
n k : ℕ
hk : k ∈ Icc 1 n
⊢ (if k = 0 then 0 else f k) = f k
have rw : f k = f k
Tactic: rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) 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 this : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) (∑ k ∈ Icc 1 n, f k)
Tactic: have (n : _) : ∑ k ∈ Icc 1 n, (if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k :=
    Finset.sum_congr rfl fun k hk ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
this : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 1 n, if k = 0 then 0 else 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 rw : (s *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      (∑ k ∈ Icc 1 ⌊t⌋₊, if k = 0 then 0 else f k) * (↑t : ℂ) ^ (-(s + 1))) =
  s *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
Tactic: rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
this : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) (∑ k ∈ Icc 1 n, f k)
rw :
  (s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, if k = 0 then 0 else f k) * (↑t : ℂ) ^ (-(s + 1))) =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 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 rw₁ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) r
Tactic: rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) s
hO : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
this : ∀ (n : ℕ), Eq (α := ℂ) (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) (∑ k ∈ Icc 1 n, f k)
rw :
  (s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, if k = 0 then 0 else f k) * (↑t : ℂ) ^ (-(s + 1))) =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))
rw₁ :
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, if k = 0 then 0 else 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₂ : ∀ {n : ℕ}, n ≠ 0 → ¬n = 0
Tactic: rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
have simp_rw : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume
have refine : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
Tactic: refine locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
  ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) t
Tactic: refine ContinuousOn.locallyIntegrableOn (fun t ht ↦ ?_) measurableSet_Ici
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
have h₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
Tactic: have h₁ : LocallyIntegrableOn (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (t : ℂ) ^ (-(s : ℂ) - 1))
        (Set.Ici 1) := by
    simp_rw [mul_comm]
    refine locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_
    refine ContinuousOn.locallyIntegrableOn (fun t ht ↦ ?_) measurableSet_Ici
    exact (continuousAt_ofReal_cpow_const _ _ <|
      Or.inr (zero_lt_one.trans_le ht).ne').continuousWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
have simp_rw : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ t
Tactic: simp_rw [Real.rpow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ t
have refine : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ)
Tactic: refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ)
have this : Tendsto (fun (n : ℕ) ↦ (∑ k ∈ Icc 1 n, f k) / (↑(HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1) : ℂ)) atTop (𝓝 l)
Tactic: have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
      simpa using hlim
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
have h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
Tactic: have h₂ : (fun t : ℝ ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ (1 : ℝ) := by
    simp_rw [Real.rpow_one]
    refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor
    have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
      simpa using hlim
    simpa using (isBigO_atTop_natCast_rpow_of_tendsto_div_rpow this).comp_tendsto
        tendsto_nat_floor_atTop
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
have refine_1 : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦
  t ^ (-s)
Tactic: refine h₁.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
refine_1 :
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦
    t ^ (-s)
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
have refine_2 : IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume
Tactic: refine h₁.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ 1 + (-s - 1) ≤ -s
have linarith : -s < 1 + (-s - 1) → -s - (1 + (-s - 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦
    t ^ (-s)
have refine_1 : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦ t ^ (-s - 1)
Tactic: refine IsBigO.mul_atTop_rpow_of_isBigO_rpow 1 (-s - 1) _ h₂ ?_ (by linarith)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume
have refine_2 : -s < -1
Tactic: rwa [integrableAtFilter_rpow_atTop_iff, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
have refine : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (-s - 1)) (Set.Ici 1)
Tactic: refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
have h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
Tactic: have h : LocallyIntegrableOn (fun t : ℝ ↦ ‖S t‖ * (t ^ (-s - 1))) (Set.Ici 1) := by
    refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici
    exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
have refine_1 : ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖
Tactic: refine h.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) (isBigO_iff.mpr ⟨ε, ?_⟩) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
refine_1 : ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
have refine_2 : IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume
Tactic: refine h.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) (isBigO_iff.mpr ⟨ε, ?_⟩) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖
have h₁ : ∀ (t : ℝ) (ht : T ≤ t) (ht' : 0 < t), ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖
Tactic: filter_upwards [eventually_ge_atTop T, eventually_gt_atTop 0] with t ht ht'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
have refine : EventuallyEq (β := ℂ) atTop
  (fun (x : ℝ) ↦
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) x *
      (↑((↑⌊x⌋₊ : ℝ) / x) : ℂ))
  fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)
Tactic: refine (mul_one l ▸ ofReal_one ▸ ((hlim.comp tendsto_nat_floor_atTop).mul <|
      tendsto_ofReal_iff.mpr <| tendsto_nat_floor_div_atTop)).congr' ?_