awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (HPow.hPow (α := ℂ) (↑n : ℂ) k)⁻¹

Tactic:
exact (Summable.of_nat_of_neg (by simp [hkk]) (by simp [hkk])).of_norm

Premises used: Summable.of_norm, Summable.of_nat_of_neg
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1)

Tactic:
hurwitzZetaEven_residue_one 0

Premises used: riemannZeta, OfNat.ofNat, HurwitzZeta.hurwitzZetaEven_residue_one
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1)

Tactic:
exact hurwitzZetaEven_residue_one 0

Premises used: OfNat.ofNat, HurwitzZeta.hurwitzZetaEven_residue_one
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) (𝓝[{s : ℂ | 1 < s.re}] 1)
    (𝓝 1)

Tactic:
(tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_

Premises used: tendsto_nhdsWithin_mono_left, Filter.Tendsto.congr', riemannZeta_residue_one
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
refine_1 : Subset (α := Set ℂ) {s : ℂ | 1 < s.re} {1}ᶜ
refine_2 :
  EventuallyEq (β := ℂ) (𝓝[{s : ℂ | 1 < s.re}] 1) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) fun (s : ℂ) ↦
    (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) (𝓝[{s : ℂ | 1 < s.re}] 1)
    (𝓝 1)

Tactic:
refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_

Premises used: tendsto_nhdsWithin_mono_left, Filter.Tendsto.congr', riemannZeta_residue_one
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ Subset (α := Set ℂ) {s : ℂ | 1 < s.re} {1}ᶜ

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
s : ℂ
hs : 1 < s.re
⊢ (s - 1) * riemannZeta s = (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs

Premises used: zeta_eq_tsum_one_div_nat_cpow, congr_arg
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
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
h₁ h₂ : ∀ (s : ℂ) (hs : 1 < s.re), (s - 1) * riemannZeta s = (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ EventuallyEq (β := ℂ) (𝓝[{s : ℂ | 1 < s.re}] 1) (fun (s : ℂ) ↦ (s - 1) * riemannZeta s) fun (s : ℂ) ↦
    (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
filter_upwards [eventually_mem_nhdsWithin] with s hs using
      congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs

Premises used: eventually_mem_nhdsWithin, congr_arg
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
rw : Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑((x - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)) (𝓝[>] 1) (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (s : ℝ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s) (𝓝[>] 1) (𝓝 1)

Tactic:
rw [← tendsto_ofReal_iff, ofReal_one]

Premises used: Filter.tendsto_ofReal_iff, Complex.ofReal_one
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | 1 < s.re} (↑x : ℂ)

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
⊢ 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)
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ (↑s : ℂ)) (𝓝[>] 1) (𝓝[{s : ℂ | 1 < s.re}] 1)
apply :
  ∀ (s : ℝ),
    ((fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) ∘ fun (s : ℝ) ↦ (↑s : ℂ)) s =
      (↑((s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ)
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑((x - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)) (𝓝[>] 1) (𝓝 1)

Tactic:
apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_

Premises used: tendsto_sub_mul_tsum_nat_cpow, Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.RiemannZeta
Goal:
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ (↑s : ℂ)) (𝓝[>] 1) (𝓝[{s : ℂ | 1 < s.re}] 1)
s : ℝ
⊢ ((fun (s : ℂ) ↦ (s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) s) ∘ fun (s : ℝ) ↦ (↑s : ℂ)) s =
    (↑((s - 1) * ∑' (n : ℕ), 1 / HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ)

Tactic:
simp only [one_div, Function.comp_apply, ofReal_mul, ofReal_sub, ofReal_one, ofReal_tsum,
    ofReal_inv, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast]

Premises used: Nat.cast_nonneg, Complex.ofReal_cpow, Complex.ofReal_one, one_div, Complex.ofReal_natCast, Complex.ofReal_sub, Function.comp_apply, Complex.ofReal_tsum, Complex.ofReal_inv, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
⊢ -s ≠ 0

Tactic:
have h₁ : -s ≠ 0 := neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
rw : r ≤ s.re
⊢ (-s).re + r ≤ 0

Tactic:
rw [neg_re, neg_add_nonpos_iff]

Premises used: Complex.neg_re, neg_add_nonpos_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
⊢ r ≤ s.re

Tactic:
hs.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
⊢ r ≤ s.re

Tactic:
exact hs.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

Tactic:
have h₂ : (-s).re + r ≤ 0 := by
    rw [neg_re, neg_add_nonpos_iff]
    exact hs.le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
⊢ ∀ (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'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ∀ (t : ℝ) (ht : 0 < t), deriv (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ (-s)‖) fun (t : ℝ) ↦ -s.re * t ^ (-(s.re + 1))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

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

Tactic:
rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']

Premises used: deriv_norm_ofReal_cpow, neg_add', Complex.neg_re
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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))

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']
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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))
simp_rw : Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x
⊢ LSeriesSummable f s

Tactic:
simp_rw [LSeriesSummable, funext (LSeries.term_def₀ hf s), mul_comm (f _)]

Premises used: funext, mul_comm, LSeries.term_def₀, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

Tactic:
summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_

Premises used: summable_mul_of_bigO_atTop'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
refine_4 :
  IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)) atTop volume
⊢ Summable (α := ℂ) fun (x : ℕ) ↦ HPow.hPow (α := ℂ) (↑x : ℂ) (-s) * f x

Tactic:
refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_

Premises used: summable_mul_of_bigO_atTop'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

Tactic:
(Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi
      (integrableOn_Ioi_deriv_norm_ofReal_cpow zero_lt_one ?_)).locallyIntegrableOn

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.locallyIntegrableOn, zero_lt_one, integrableOn_Ici_iff_integrableOn_Ioi, integrableOn_Ioi_deriv_norm_ofReal_cpow
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : (-s).re ≤ 0
⊢ LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) t))
    (Set.Ici 1) volume

Tactic:
refine (Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi
      (integrableOn_Ioi_deriv_norm_ofReal_cpow zero_lt_one ?_)).locallyIntegrableOn

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.locallyIntegrableOn, zero_lt_one, integrableOn_Ici_iff_integrableOn_Ioi, integrableOn_Ioi_deriv_norm_ofReal_cpow
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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))
⊢ (-s).re ≤ 0

Tactic:
exact neg_re _ ▸ neg_nonpos.mpr <| hr.trans hs.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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))
⊢ ∀ (x : ℕ), HPow.hPow (α := ℝ) (β := ℝ) (↑x : ℝ) 0 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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_2 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ))) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ norm (E := ℂ) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (-s)) (↑n : ℝ)) * ∑ k ∈ Icc 1 n, ‖f k‖) fun (x : ℕ) ↦ 1

Tactic:
refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow _ _ _ ?_ hO h₂).congr_right (by simp)

Premises used: Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow, Asymptotics.IsBigO.congr_right
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ℝ))) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re

Tactic:
(norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

Premises used: Filter.EventuallyEq.isBigO, Complex.norm_ofReal_cpow_eventually_eq_atTop, Asymptotics.IsBigO.natCast_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ℝ))) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (-s).re

Tactic:
exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

Premises used: Filter.EventuallyEq.isBigO, Complex.norm_ofReal_cpow_eventually_eq_atTop, Asymptotics.IsBigO.natCast_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)

Tactic:
h₄.isBigO.of_const_mul_right.mul_atTop_rpow_of_isBigO_rpow _ r _ ?_ le_rfl

Premises used: Filter.EventuallyEq.isBigO, le_rfl, Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow, Asymptotics.IsBigO.of_const_mul_right
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) fun (t : ℝ) ↦ t ^ r
⊢ 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 h₄.isBigO.of_const_mul_right.mul_atTop_rpow_of_isBigO_rpow _ r _ ?_ le_rfl

Premises used: Filter.EventuallyEq.isBigO, le_rfl, Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow, Asymptotics.IsBigO.of_const_mul_right
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) fun (t : ℝ) ↦ t ^ r

Tactic:
(hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
      isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)

Premises used: Multiset.sum, Multiset.foldr, Asymptotics.IsEquivalent.isBigO, Asymptotics.IsBigO.trans, tendsto_nat_floor_atTop, Filter.eventually_ge_atTop, Asymptotics.IsBigO.rpow, Asymptotics.IsBigO.comp_tendsto, OfNat.ofNat, Finset.sum
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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 : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) fun (t : ℝ) ↦ t ^ r

Tactic:
exact (hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
      isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsBigO.trans, tendsto_nat_floor_atTop, Filter.eventually_ge_atTop, Asymptotics.IsBigO.rpow, Asymptotics.IsBigO.comp_tendsto, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
refine_4₁ : r < s.re + 1 + -1
refine_4₂ refine_4₃ refine_4₄ refine_4₅ : r < s.re
⊢ IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (-(s.re + 1) + r)) atTop volume

Tactic:
rwa [integrableAtFilter_rpow_atTop_iff, neg_add_lt_iff_lt_add, add_neg_cancel_right]

Premises used: neg_add_lt_iff_lt_add, add_neg_cancel_right, integrableAtFilter_rpow_atTop_iff
-- 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
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then 0 else f n) = f n

Tactic:
simp_rw [if_neg hn]

Premises used: if_neg