awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ LocallyIntegrableOn (X := ℝ) (ε := ℂ) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (Set.Ici 1) volume

Tactic:
refine (Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi <|
      integrableOn_Ioi_deriv_ofReal_cpow zero_lt_one
        (by simpa using hr.trans_lt hs)).locallyIntegrableOn

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.locallyIntegrableOn, integrableOn_Ioi_deriv_ofReal_cpow, zero_lt_one, integrableOn_Ici_iff_integrableOn_Ioi
-- 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
rwa rwa₁ rwa₂ rwa₃ : r < s.re
⊢ 0 < s.re - r

Tactic:
rwa [sub_pos]

Premises used: sub_pos
-- 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 : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)

Tactic:
have hlim : Tendsto (fun n : ℕ ↦ (n : ℝ) ^ (-(s.re - r))) atTop (𝓝 0) :=
      (tendsto_rpow_neg_atTop (by rwa [sub_pos])).comp tendsto_natCast_atTop_atTop
-- 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
hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
    atTop (𝓝 0)

Tactic:
(IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow (-s.re) _ _ ?_ hO ?_).trans_tendsto hlim

Premises used: Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow, Complex.re, Asymptotics.IsBigO.trans_tendsto, Neg.neg
-- 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
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)
convert_2₁ : -s.re + r ≤ -(s.re - r)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ HMul.hMul (α := ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) (∑ k ∈ Icc 0 n, f k))
    atTop (𝓝 0)

Tactic:
refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow (-s.re) _ _ ?_ hO ?_).trans_tendsto hlim

Premises used: Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow, Complex.re, Asymptotics.IsBigO.trans_tendsto, Neg.neg
-- 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
hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re)

Tactic:
isBigO_norm_left.mp <| (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

Premises used: Filter.EventuallyEq.isBigO, Complex.norm_ofReal_cpow_eventually_eq_atTop, Asymptotics.isBigO_norm_left, Asymptotics.IsBigO.natCast_atTop, Iff.mp
-- 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
hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ (fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) (↑n : ℝ)) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re)

Tactic:
exact isBigO_norm_left.mp <| (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

Premises used: Filter.EventuallyEq.isBigO, Complex.norm_ofReal_cpow_eventually_eq_atTop, Asymptotics.isBigO_norm_left, Asymptotics.IsBigO.natCast_atTop, Iff.mp
-- 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
hlim : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re - r))) atTop (𝓝 0)
linarith : -(s.re - r) < -s.re + r → -(s.re - r) - (-s.re + r) = 0
⊢ -s.re + r ≤ -(s.re - r)

Tactic:
linarith
-- 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 : (-(s + 1)).re + r ≤ (-s - 1).re + r
rw₁ rw₂ : (-s - 1).re + r ≤ (-s - 1).re + r
⊢ -(s + 1).re + r ≤ (-s - 1).re + r

Tactic:
rw [← neg_re, neg_add']

Premises used: neg_add', Complex.neg_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
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)
convert_3₁ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 0 ⌊t⌋₊, f k) fun (t : ℝ) ↦ t ^ 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)

Tactic:
refine .mul_atTop_rpow_of_isBigO_rpow (-(s + 1).re) r _ ?_ ?_ (by rw [← neg_re, neg_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
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 (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ (-s)) fun (t : ℝ) ↦ t ^ (-(s + 1).re)

Tactic:
simpa [-neg_add_rev, neg_add'] using isBigO_deriv_ofReal_cpow_const_atTop _

Premises used: neg_add_rev, neg_add', isBigO_deriv_ofReal_cpow_const_atTop
-- 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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 0 ⌊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, List.foldr, Finset.sum
-- 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
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 0 ⌊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 : ℝ
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
n : ℕ
h : n ≠ 0
⊢ (if n = 0 then 0 else f n) = f n

Tactic:
if_neg h

Premises used: if_neg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
h₁ h₂ : ∀ (n : ℕ) (h : 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 h using if_neg h

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

Premises used: LSeriesSummable_congr'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
hS₁ : LSeriesSummable (fun (n : ℕ) ↦ if n = 0 then 0 else f n) s
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r

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

Premises used: LSeriesSummable_congr'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
rw rw₁ : f k = f k
⊢ (if k = 0 then 0 else f k) = f k

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).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:
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 : ℕ), 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']
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
rw₂ : ∀ {n : ℕ}, n ≠ 0 → ¬n = 0
⊢ LSeries f s =
    s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(s + 1))

Tactic:
rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS]

Premises used: LSeries_congr, _private.0.LSeries_eq_mul_integral_aux, if_neg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
⊢ (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:
simp_all
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
⊢ 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:
simp_all
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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)
⊢ ∀ {n : ℕ}, n ≠ 0 → ¬n = 0

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
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))

Tactic:
LSeries_eq_mul_integral _ hr hs (LSeriesSummable_of_sum_norm_bigO hO hr hs) <|
    (isBigO_of_le _ fun _ ↦ (norm_sum_le _ _).trans <| Real.le_norm_self _).trans hO

Premises used: Norm.norm, Asymptotics.IsBigO.trans, LSeries_eq_mul_integral, LSeriesSummable_of_sum_norm_bigO, Real.le_norm_self, LE.le.trans, Asymptotics.isBigO_of_le, norm_sum_le, Finset.sum
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℝ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hO : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ k ∈ Icc 1 n, f k) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) r
hf : ∀ (n : ℕ), 0 ≤ f n
x : ℕ
⊢ Eq (α := ℝ) (∑ k ∈ Icc 1 x, f k) (∑ k ∈ Icc 1 x, ‖(↑(f k) : ℂ)‖)

Tactic:
simp [abs_of_nonneg (hf _)]

Premises used: abs_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
simp_rw :
  LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume

Tactic:
simp_rw [mul_comm]

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

Tactic:
locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_

Premises used: zero_le_one, locallyIntegrableOn_mul_sum_Icc
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
refine : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume

Tactic:
refine locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_

Premises used: zero_le_one, locallyIntegrableOn_mul_sum_Icc
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

Tactic:
ContinuousOn.locallyIntegrableOn (fun t ht ↦ ?_) measurableSet_Ici

Premises used: ContinuousOn.locallyIntegrableOn, measurableSet_Ici
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t),
    ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) t
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume

Tactic:
refine ContinuousOn.locallyIntegrableOn (fun t ht ↦ ?_) measurableSet_Ici

Premises used: ContinuousOn.locallyIntegrableOn, measurableSet_Ici
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t
⊢ ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) t

Tactic:
(continuousAt_ofReal_cpow_const _ _ <|
      Or.inr (zero_lt_one.trans_le ht).ne').continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
s : ℝ
hs : 1 < s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Ici 1) t
⊢ ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) t

Tactic:
exact (continuousAt_ofReal_cpow_const _ _ <|
      Or.inr (zero_lt_one.trans_le ht).ne').continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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

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
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
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
simp_rw : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ t
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1

Tactic:
simp_rw [Real.rpow_one]

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

Tactic:
IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor

Premises used: Asymptotics.isEquivalent_nat_floor, Asymptotics.IsBigO.trans_isEquivalent