awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
h₁ h₂ : ∀ (n : ℕ) (hn : n ≠ 0), (if n = 0 then 0 else f n) = f n
⊢ (fun (n : ℕ) ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn using by simp_rw [if_neg hn]

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

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]
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

Tactic:
(LSeriesSummable_of_sum_norm_bigO_aux (if_pos rfl) ?_ hr hs).congr' _ h₁

Premises used: LSeriesSummable.congr', _private.0.LSeriesSummable_of_sum_norm_bigO_aux
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
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
⊢ LSeriesSummable f s

Tactic:
refine (LSeriesSummable_of_sum_norm_bigO_aux (if_pos rfl) ?_ hr hs).congr' _ h₁

Premises used: LSeriesSummable.congr', _private.0.LSeriesSummable_of_sum_norm_bigO_aux
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

Tactic:
hO.congr' (Eventually.of_forall fun _ ↦ Finset.sum_congr rfl fun _ h ↦ ?_) EventuallyEq.rfl

Premises used: Filter.Eventually.of_forall, Asymptotics.IsBigO.congr', Filter.EventuallyEq.rfl, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
refine : ∀ (x x_1 : ℕ) (h : x_1 ∈ Icc 1 x), ‖f x_1‖ = ‖if x_1 = 0 then 0 else f x_1‖
⊢ 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 hO.congr' (Eventually.of_forall fun _ ↦ Finset.sum_congr rfl fun _ h ↦ ?_) EventuallyEq.rfl

Premises used: Filter.Eventually.of_forall, Asymptotics.IsBigO.congr', Filter.EventuallyEq.rfl, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
rw rw₁ : ‖f x_1‖ = ‖f x_1‖
⊢ ‖f x_1‖ = ‖if x_1 = 0 then 0 else f x_1‖

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Premises used: Finset.mem_Icc, LT.lt.ne', zero_lt_one, And.left, LT.lt.trans_le, Iff.mp, if_neg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
r : ℝ
s : ℂ
f : ℕ → ℝ
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hf : ∀ (n : ℕ), 0 ≤ f n
hr : 0 ≤ r
hs : r < s.re
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, ‖(↑(f k) : ℂ)‖) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) r

Tactic:
simpa [abs_of_nonneg (hf _)]

Premises used: abs_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
rwa₄ : r < 1 + s.re + -1
rwa₅ rwa₆ rwa₇ rwa₈ : r < s.re
⊢ (-s - 1).re + r < -1

Tactic:
rwa [sub_re, one_re, neg_re, neg_sub_left, neg_add_lt_iff_lt_add, add_neg_cancel_comm]

Premises used: neg_add_lt_iff_lt_add, neg_sub_left, Complex.sub_re, Complex.neg_re, add_neg_cancel_comm, Complex.one_re
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

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]
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
⊢ s ≠ 0

Tactic:
have h₂ : s ≠ 0 := ne_zero_of_re_pos (hr.trans_lt hs)
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
⊢ ∀ (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₂)
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ℕ
⊢ 0 ∉ Icc (HAdd.hAdd (α := ℕ) 0 1) n

Tactic:
aesop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
rw₄ rw₅ : Eq (α := ℂ) (∑ x ∈ Icc 1 n, f x) (∑ k ∈ Icc 1 n, f k)
⊢ Eq (α := ℂ) (∑ k ∈ Icc 0 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]

Premises used: Nat.zero_le, zero_add, Finset.insert_Icc_add_one_left_eq_Icc, Finset.sum_insert
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)

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]
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r

Tactic:
simp_rw [← h₄] at hO
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 :
  LSeries f s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (a : ℝ) ↦
      s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * (↑a : ℂ) ^ (-(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))

Tactic:
rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)))

Tactic:
tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).mpr hS.hasSum.tendsto_sum_nat) ?_

Premises used: Iff.mpr, HasSum.tendsto_sum_nat, Summable.hasSum, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
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)))))
⊢ 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:
refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).mpr hS.hasSum.tendsto_sum_nat) ?_

Premises used: Iff.mpr, HasSum.tendsto_sum_nat, Summable.hasSum, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
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)))))
⊢ 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:
simp_rw [Nat.range_succ_eq_Icc_zero, LSeries.term_def₀ hf, mul_comm (f _)]

Premises used: Nat.range_succ_eq_Icc_zero, mul_comm, LSeries.term_def₀
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ℕ) ↦ ∑ k ∈ Icc 0 n, (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑k : ℝ) * f k) atTop
    (𝓝
      (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:
tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)

Premises used: Iff.mpr, tendsto_sum_mul_atTop_nhds_one_sub_integral₀, integrableAtFilter_rpow_atTop_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
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)
⊢ 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:
convert!
    tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)

Premises used: Iff.mpr, tendsto_sum_mul_atTop_nhds_one_sub_integral₀, integrableAtFilter_rpow_atTop_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 :
  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))
⊢ (@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:
rw [zero_sub, ← integral_neg]

Premises used: MeasureTheory.integral_neg, zero_sub
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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))

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 :
  ∀ (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)
⊢ 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:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
h₅ : -s ≠ 0
⊢ 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:
rw [deriv_ofReal_cpow_const (zero_lt_one.trans ht).ne', h₄]

Premises used: Complex.deriv_ofReal_cpow_const, LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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))) = -(-s * (↑t : ℂ) ^ (-s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 ≠ 0

Tactic:
neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)

Premises used: Iff.mpr, neg_ne_zero, Complex.ne_zero_of_re_pos, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 ≠ 0

Tactic:
exact neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)

Premises used: Iff.mpr, neg_ne_zero, Complex.ne_zero_of_re_pos, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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).re < 0

Tactic:
simpa using hr.trans_lt hs

Premises used: LE.le.trans_lt