awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ t

Tactic:
refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor

Premises used: Asymptotics.IsBigO.trans_isEquivalent
-- 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
⊢ Tendsto (fun (n : ℕ) ↦ (∑ k ∈ Icc 1 n, f k) / (↑(HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1) : ℂ)) atTop (𝓝 l)

Tactic:
simpa using hlim
-- 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
⊢ Tendsto (fun (n : ℕ) ↦ (∑ k ∈ Icc 1 n, f k) / (↑(HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1) : ℂ)) atTop (𝓝 l)

Tactic:
have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
      simpa using hlim
-- 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
this : Tendsto (fun (n : ℕ) ↦ (∑ k ∈ Icc 1 n, f k) / (↑(HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1) : ℂ)) atTop (𝓝 l)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ)

Tactic:
simpa using (isBigO_atTop_natCast_rpow_of_tendsto_div_rpow this).comp_tendsto
        tendsto_nat_floor_atTop

Premises used: tendsto_nat_floor_atTop, Asymptotics.isBigO_atTop_natCast_rpow_of_tendsto_div_rpow, Asymptotics.IsBigO.comp_tendsto
-- 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 : ℝ) ↦ HPow.hPow (β := ℝ) t 1

Tactic:
have h₂ : (fun t : ℝ ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ (1 : ℝ) := by
    simp_rw [Real.rpow_one]
    refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor
    have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
      simpa using hlim
    simpa using (isBigO_atTop_natCast_rpow_of_tendsto_div_rpow this).comp_tendsto
        tendsto_nat_floor_atTop
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume

Tactic:
h₁.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) ?_ ?_

Premises used: MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
refine_1 :
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦
    t ^ (-s)
refine_2 : IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) (Set.Ici 1) volume

Tactic:
refine h₁.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) ?_ ?_

Premises used: MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
linarith : -s < 1 + (-s - 1) → -s - (1 + (-s - 1)) = 0
⊢ 1 + (-s - 1) ≤ -s

Tactic:
linarith
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
refine_1 : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦ t ^ (-s - 1)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦
    t ^ (-s)

Tactic:
refine IsBigO.mul_atTop_rpow_of_isBigO_rpow 1 (-s - 1) _ h₂ ?_ (by linarith)

Premises used: HSub.hSub, Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow, OfNat.ofNat, Neg.neg
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦ t ^ (-s - 1)

Tactic:
(norm_ofReal_cpow_eventually_eq_atTop _).isBigO.of_norm_left

Premises used: Filter.EventuallyEq.isBigO, Complex.norm_ofReal_cpow_eventually_eq_atTop, Asymptotics.IsBigO.of_norm_left
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) fun (t : ℝ) ↦ t ^ (-s - 1)

Tactic:
exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.of_norm_left

Premises used: Filter.EventuallyEq.isBigO, Complex.norm_ofReal_cpow_eventually_eq_atTop, Asymptotics.IsBigO.of_norm_left
-- 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
h₂ : IsBigO (E := ℂ) (F := ℝ) atTop (fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) fun (t : ℝ) ↦ HPow.hPow (β := ℝ) t 1
refine_2 : -s < -1
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : 1 < s
⊢ IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume

Tactic:
rwa [integrableAtFilter_rpow_atTop_iff, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, integrableAtFilter_rpow_atTop_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici

Premises used: isLocallyClosed_Ici, MeasureTheory.LocallyIntegrableOn.mul_continuousOn, MeasureTheory.LocallyIntegrableOn.norm
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
refine : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (-s - 1)) (Set.Ici 1)
⊢ LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici

Premises used: isLocallyClosed_Ici, MeasureTheory.LocallyIntegrableOn.mul_continuousOn, MeasureTheory.LocallyIntegrableOn.norm
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (-s - 1)) (Set.Ici 1)

Tactic:
fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Premises used: Real.continuousAt_rpow_const, ContinuousAt.continuousWithinAt, HSub.hSub, LT.lt.ne', zero_lt_one, LT.lt.trans_le, ContinuousOn, Or.inl, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (-s - 1)) (Set.Ici 1)

Tactic:
exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Premises used: Real.continuousAt_rpow_const, ContinuousAt.continuousWithinAt, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
have h : LocallyIntegrableOn (fun t : ℝ ↦ ‖S t‖ * (t ^ (-s - 1))) (Set.Ici 1) := by
    refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici
    exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
h.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) (isBigO_iff.mpr ⟨ε, ?_⟩) ?_

Premises used: Iff.mpr, Asymptotics.isBigO_iff, Exists.intro, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
refine_1 : ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖
refine_2 : IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
refine h.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) (isBigO_iff.mpr ⟨ε, ?_⟩) ?_

Premises used: Iff.mpr, Asymptotics.isBigO_iff, Exists.intro, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₁ : ∀ (t : ℝ) (ht : T ≤ t) (ht' : 0 < t), ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖
⊢ ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖

Tactic:
filter_upwards [eventually_ge_atTop T, eventually_gt_atTop 0] with t ht ht'

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
ht' : 0 < t
⊢ ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖

Tactic:
simpa [abs_of_nonneg, Real.rpow_nonneg, ht'.le, Real.rpow_sub ht', mul_assoc, ht'.ne',
      mul_div_cancel₀] using mul_le_mul_of_nonneg_right (hS₂ t ht) (norm_nonneg <| t ^ (-s - 1))

Premises used: mul_assoc, HSub.hSub, LT.lt.le, mul_div_cancel₀, LT.lt.ne', mul_le_mul_of_nonneg_right, HPow.hPow, abs_of_nonneg, Real.rpow_nonneg, Real.rpow_sub, OfNat.ofNat, norm_nonneg, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume

Tactic:
integrableAtFilter_rpow_atTop_iff.mpr <| neg_lt_neg_iff.mpr hs

Premises used: Iff.mpr, neg_lt_neg_iff, integrableAtFilter_rpow_atTop_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableAtFilter (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (-s)) atTop volume

Tactic:
exact integrableAtFilter_rpow_atTop_iff.mpr <| neg_lt_neg_iff.mpr hs

Premises used: Iff.mpr, neg_lt_neg_iff, integrableAtFilter_rpow_atTop_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
refine :
  EventuallyEq (β := ℂ) atTop
    (fun (x : ℝ) ↦
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) x *
        (↑((↑⌊x⌋₊ : ℝ) / x) : ℂ))
    fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)
⊢ Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)

Tactic:
refine (mul_one l ▸ ofReal_one ▸ ((hlim.comp tendsto_nat_floor_atTop).mul <|
      tendsto_ofReal_iff.mpr <| tendsto_nat_floor_div_atTop)).congr' ?_
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h :
  ∀ (t : ℝ) (ht : 1 ≤ t),
    ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) t *
        (↑((↑⌊t⌋₊ : ℝ) / t) : ℂ) =
      (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)
⊢ EventuallyEq (β := ℂ) atTop
    (fun (x : ℝ) ↦
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) x *
        (↑((↑⌊x⌋₊ : ℝ) / x) : ℂ))
    fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)

Tactic:
filter_upwards [eventually_ge_atTop 1] with t ht

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
t : ℝ
ht : 1 ≤ t
⊢ Ne (α := ℂ) (↑⌊t⌋₊ : ℂ) 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
t : ℝ
ht : 1 ≤ t
⊢ ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) ∘ fun (x : ℝ) ↦ ⌊x⌋₊) t * (↑((↑⌊t⌋₊ : ℝ) / t) : ℂ) =
    (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)

Tactic:
simp [div_mul_div_cancel₀ (show (⌊t⌋₊ : ℂ) ≠ 0 by simpa)]

Premises used: div_mul_div_cancel₀
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)

Tactic:
have h_lim' : Tendsto (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k : ℂ) / t) atTop (𝓝 l) := by
    refine (mul_one l ▸ ofReal_one ▸ ((hlim.comp tendsto_nat_floor_atTop).mul <|
      tendsto_ofReal_iff.mpr <| tendsto_nat_floor_div_atTop)).congr' ?_
    filter_upwards [eventually_ge_atTop 1] with t ht
    simp [div_mul_div_cancel₀ (show (⌊t⌋₊ : ℂ) ≠ 0 by simpa)]
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
h :
  ∀ (t : ℝ) (ht₁ : 0 < t) (ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε),
    ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ∀ᶠ (t : ℝ) in atTop, ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t

Tactic:
filter_upwards [eventually_gt_atTop 0, Metric.tendsto_nhds.mp h_lim' ε hε] with t ht₁ ht₂

Premises used: Metric.tendsto_nhds, Iff.mp, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun (t : ℝ) ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ)) l < ε
h : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) / (↑t : ℂ) - l‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₁ : ∀ (ht₂ : ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l) / (↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₂ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖(↑t : ℂ)‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₃ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / ‖t‖ < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₄ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - (↑t : ℂ) * l‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₅ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ / t < ε), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
h₆ h₇ h₈ h₉ : ∀ (ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t), ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * (↑t : ℂ)‖ < ε * t

Tactic:
rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
    Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂

Premises used: dist_eq_norm, LT.lt.le, Complex.norm_real, div_lt_iff₀, norm_div, mul_comm, Complex.ne_zero_of_re_pos, div_sub', Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
⊢ 0 < T

Tactic:
have hT₀ : 0 < T := zero_lt_one.trans_le hT₁
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
t : ℝ
ht : 0 < t
rw : t ^ (-s) = t * (t ^ (-s) / HPow.hPow (β := ℝ) t 1)
rw₁ : t ^ (-s) = t * (t ^ (-s) / t)
rw₂ rw₃ : t ^ (-s) = t ^ (-s)
⊢ t ^ (-s) = t * t ^ (-s - 1)

Tactic:
rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']

Premises used: Real.rpow_one, mul_div_cancel₀, LT.lt.ne', Real.rpow_sub
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
⊢ ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)

Tactic:
have h {t : ℝ} (ht : 0 < t) : t ^ (-s) = t * t ^ (-s - 1) := by
    rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)

Tactic:
mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le

Premises used: LT.lt.le, measurableSet_Ioi, mul_le_mul_of_nonneg_left, MeasureTheory.setIntegral_mono_on, sub_pos_of_lt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioi T) volume
refine_2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ε * t ^ (-s)) (Set.Ioi T) volume
refine_3 : ∀ (t : ℝ) (ht : t ∈ Set.Ioi T), ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦ ε * t ^ (-s)

Tactic:
refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le

Premises used: LT.lt.le, measurableSet_Ioi, mul_le_mul_of_nonneg_left, MeasureTheory.setIntegral_mono_on, sub_pos_of_lt
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioi T) volume

Tactic:
(lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁

Premises used: _private.0.lemma₂, Iff.mpr, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ici_iff
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * (↑t : ℂ)‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioi T) volume

Tactic:
exact (lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁

Premises used: _private.0.lemma₂, Iff.mpr, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ici_iff