awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
refine_1 : Subset (α := Set ℂ) {s : ℂ | 1 < s.re} {1}ᶜ
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) (𝓝[{s : ℂ | 1 < s.re}] 1)
    (𝓝 1)
have refine_2 : EventuallyEq (β := ℂ) (𝓝[{s : ℂ | 1 < s.re}] 1) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) fun (s : ℂ) ↦
  (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ EventuallyEq (β := ℂ) (𝓝[{s : ℂ | 1 < s.re}] 1) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) fun (s : ℂ) ↦
    (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have h : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {s : ℂ | 1 < s.re} x) x} x →
        Membership.mem (γ := Set ℂ)
          {x : ℂ |
            (fun (x : ℂ) ↦
                Eq (α := ℂ) ((fun (s : ℂ) ↦ (s - 1) * riemannZeta s) x)
                  ((fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) x))
              x}
          x}
    a
Tactic: filter_upwards [eventually_mem_nhdsWithin] with s hs using
      congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {s : ℂ | 1 < s.re} x) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ |
              (fun (x : ℂ) ↦
                  Eq (α := ℂ) ((fun (s : ℂ) ↦ (s - 1) * riemannZeta s) x)
                    ((fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) x))
                x}
            x}
      a
⊢ EventuallyEq (β := ℂ) (𝓝[{s : ℂ | 1 < s.re}] 1) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) fun (s : ℂ) ↦
    (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
have h₁ : ∀ (a : ℂ), 1 < a.re → (a - 1) * riemannZeta a = (a - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) a
Tactic: filter_upwards [eventually_mem_nhdsWithin] with s hs using
      congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (s : ℝ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s) (𝓝[>] 1) (𝓝 1)
have rw : Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑((x - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)) (𝓝[>] 1) (𝓝 1)
Tactic: rw [← tendsto_ofReal_iff, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (hypothesis)
Goal:
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑((x - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)) (𝓝[>] 1) (𝓝 1)
have this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ (↑s : ℂ)) (𝓝[>] 1) (𝓝[{s : ℂ | 1 < s.re}] 1)
Tactic: have : Tendsto (fun s : ℝ ↦ (s : ℂ)) (𝓝[>] 1) (𝓝[{s | 1 < re s}] 1) :=
    continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin (fun _ _ ↦ by simp_all)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.RiemannZeta (goal)
Goal:
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ (↑s : ℂ)) (𝓝[>] 1) (𝓝[{s : ℂ | 1 < s.re}] 1)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑((x - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)) (𝓝[>] 1) (𝓝 1)
have apply : ∀ (s : ℝ),
  ((fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) ∘ fun (s : ℝ) ↦ (↑s : ℂ)) s =
    (↑((s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ)
Tactic: apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
⊢ LSeriesSummable f s
have h₁ : -s ≠ 0
Tactic: have h₁ : -s ≠ 0 := neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
⊢ (-s).re + r ≤ 0
have rw : r ≤ s.re
Tactic: rw [neg_re, neg_add_nonpos_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
⊢ LSeriesSummable f s
have h₂ : (-s).re + r ≤ 0
Tactic: have h₂ : (-s).re + r ≤ 0 := by
    rw [neg_re, neg_add_nonpos_iff]
    exact hs.le
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
⊢ LSeriesSummable f s
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 :=
    have ht' : t ≠ 0 := (zero_lt_one.trans_le ht).ne'
    (differentiableAt_id.ofReal_cpow_const ht' h₁).norm ℝ <|
      (cpow_ne_zero_iff_of_exponent_ne_zero h₁).mpr <| ofReal_ne_zero.mpr ht'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
have h : ∀ (t : ℝ) (ht : 0 < t), deriv (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
t : ℝ
ht : 0 < t
⊢ deriv (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))
have h : (-s).re * t ^ ((-s).re - 1) = -s.re * t ^ (-(s.re + 1))
Tactic: rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
t : ℝ
ht : 0 < t
h : (-s).re * t ^ ((-s).re - 1) = -s.re * t ^ (-(s.re + 1))
⊢ deriv (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))
have h₄ : -s.re * t ^ (-s.re - 1) = -s.re * t ^ (-(s.re + 1))
Tactic: rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
t : ℝ
ht : 0 < t
h : (-s).re * t ^ ((-s).re - 1) = -s.re * t ^ (-(s.re + 1))
h₄ : -s.re * t ^ (-s.re - 1) = -s.re * t ^ (-(s.re + 1))
⊢ deriv (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))
have h₅ : -s.re * t ^ (-s.re - 1) = -s.re * t ^ (-s.re - 1)
Tactic: rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
⊢ LSeriesSummable f s
have h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
Tactic: have h₄ : (deriv fun t : ℝ ↦ ‖(t : ℂ) ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1)) := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
⊢ LSeriesSummable f s
have simp_rw : Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x
Tactic: simp_rw [LSeriesSummable, funext (LSeries.term_def₀ hf s), mul_comm (f _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
⊢ Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x
have refine_1 : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t))
  (Set.Ici 1) volume
Tactic: refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
refine_1 :
  LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t))
    (Set.Ici 1) volume
⊢ Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop
  (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ)) * ∑ k ∈ Icc 1 n, ‖f k‖) fun (x : ℕ) ↦ 1
Tactic: refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
refine_1 :
  LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t))
    (Set.Ici 1) volume
refine_2 :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ)) * ∑ k ∈ Icc 1 n, ‖f k‖) fun (x : ℕ) ↦ 1
⊢ Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x
have refine_3 : IsBigO (E := ℝ) (F := ℝ) atTop
  (fun (t : ℝ) ↦
    HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t)) t)
      (∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖))
  fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)
Tactic: refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
refine_1 :
  LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t))
    (Set.Ici 1) volume
refine_2 :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ)) * ∑ k ∈ Icc 1 n, ‖f k‖) fun (x : ℕ) ↦ 1
refine_3 :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦
      HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t)) t)
        (∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖))
    fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)
⊢ Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x
have refine_4 : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)) atTop volume
Tactic: refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
⊢ LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t))
    (Set.Ici 1) volume
have refine_1 : (-s).re ≤ 0
Tactic: refine (Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi
      (integrableOn_Ioi_deriv_norm_ofReal_cpow zero_lt_one ?_)).locallyIntegrableOn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ)) * ∑ k ∈ Icc 1 n, ‖f k‖) fun (x : ℕ) ↦ 1
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ))) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re
Tactic: refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow _ _ _ ?_ hO h₂).congr_right (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦
      HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t)) t)
        (∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖))
    fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)
have refine_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) fun (t : ℝ) ↦ t ^ r
Tactic: refine h₄.isBigO.of_const_mul_right.mul_atTop_rpow_of_isBigO_rpow _ r _ ?_ le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
⊢ IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)) atTop volume
have refine_4 : -(s.re + 1) + r < -1
Tactic: rwa [integrableAtFilter_rpow_atTop_iff, neg_add_lt_iff_lt_add, add_neg_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (-s)‖) t
h₄ : EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))
refine_4 : -(s.re + 1) + r < -1
⊢ IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)) atTop volume
have refine_4₁ : r < s.re + 1 + -1
Tactic: rwa [integrableAtFilter_rpow_atTop_iff, neg_add_lt_iff_lt_add, add_neg_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
⊢ (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 hn using by simp_rw [if_neg hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
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 hn using by simp_rw [if_neg hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
⊢ LSeriesSummable f s
have h₁ : (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f
Tactic: have h₁ : (fun n ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f := by
    filter_upwards [eventually_ne_atTop 0] with n hn using by simp_rw [if_neg hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f
⊢ LSeriesSummable f s
have refine : 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: refine (LSeriesSummable_of_sum_norm_bigO_aux (if_pos rfl) ?_ hr hs).congr' _ h₁
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖if k = 0 then 0 else f k‖) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) r
have refine : ∀ (x x_1 : ℕ) (h : x_1 ∈ Icc 1 x), ‖f x_1‖ = ‖if x_1 = 0 then 0 else f x_1‖
Tactic: refine hO.congr' (Eventually.of_forall fun _ ↦ Finset.sum_congr rfl fun _ h ↦ ?_) EventuallyEq.rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
Goal:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖f k‖) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f
x x_1 : ℕ
h : x_1 ∈ Icc 1 x
⊢ ‖f x_1‖ = ‖if x_1 = 0 then 0 else f x_1‖
have rw : ‖f x_1‖ = ‖f x_1‖
Tactic: rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']
-- 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
⊢ (-s - 1).re + r < -1
have rwa : (-s).re - re 1 + r < -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 (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
⊢ (-s - 1).re + r < -1
have rwa₁ : (-s).re - 1 + r < -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 (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
⊢ (-s - 1).re + r < -1
have rwa₂ : -s.re - 1 + r < -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 (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
⊢ (-s - 1).re + r < -1
have rwa₃ : -(1 + s.re) + r < -1
Tactic: rwa [sub_re, one_re, neg_re, neg_sub_left, neg_add_lt_iff_lt_add, add_neg_cancel_comm]