awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ) ↦ ε * t ^ (-s)) (Set.Ioi T) volume

Tactic:
(integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) hT₀).const_mul _

Premises used: Iff.mpr, neg_lt_neg_iff, integrableOn_Ioi_rpow_of_lt, MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn
-- 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 : ℝ) ↦ ε * t ^ (-s)) (Set.Ioi T) volume

Tactic:
exact (integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) hT₀).const_mul _

Premises used: Iff.mpr, neg_lt_neg_iff, integrableOn_Ioi_rpow_of_lt, MeasureTheory.Integrable.const_mul
-- 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)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ 0 < t

Tactic:
have ht' : 0 < t := hT₀.trans 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
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
refine_3 : ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t * t ^ (-s - 1)
⊢ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
rw [h ht', ← mul_assoc]

Premises used: mul_assoc
-- 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)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
⊢ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t * t ^ (-s - 1)

Tactic:
mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)

Premises used: LT.lt.le, mul_le_mul_of_nonneg_right, Real.rpow_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
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
⊢ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ε * t * t ^ (-s - 1)

Tactic:
exact mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)

Premises used: LT.lt.le, mul_le_mul_of_nonneg_right, Real.rpow_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
hT₀ : 0 < T
h : ∀ {t : ℝ} (ht : 0 < t), t ^ (-s) = t * t ^ (-s - 1)
rw :
  ((s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (a : ℝ) ↦ a ^ (-s)) ≤
    (s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ε * t ^ (-s)) ≤
    ε *
      ((s - 1) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s))

Tactic:
rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]

Premises used: MeasureTheory.integral_const_mul, mul_assoc, mul_comm
-- 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 (a : ℝ) ↦ a ^ (-s)) ≤
    (s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)

Tactic:
mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)

Premises used: mul_nonneg, MeasureTheory.setIntegral_mono_set, LT.lt.le, HasSubset.Subset.eventuallyLE, Set.Ioi_subset_Ioi, mul_le_mul_of_nonneg_left, 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 (a : ℝ) ↦ a ^ (-s)) (Set.Ioi 1) volume
refine_2 : (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioi 1))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ a ^ (-s)
⊢ ((s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (a : ℝ) ↦ a ^ (-s)) ≤
    (s - 1) * ε *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)

Tactic:
refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)

Premises used: mul_nonneg, MeasureTheory.setIntegral_mono_set, LT.lt.le, HasSubset.Subset.eventuallyLE, Set.Ioi_subset_Ioi, mul_le_mul_of_nonneg_left, 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 (a : ℝ) ↦ a ^ (-s)) (Set.Ioi 1) volume

Tactic:
integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one

Premises used: Iff.mpr, neg_lt_neg_iff, integrableOn_Ioi_rpow_of_lt, zero_lt_one
-- 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 (a : ℝ) ↦ a ^ (-s)) (Set.Ioi 1) volume

Tactic:
exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one

Premises used: Iff.mpr, neg_lt_neg_iff, integrableOn_Ioi_rpow_of_lt, zero_lt_one
-- 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)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioi 1))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ a ^ (-s)

Tactic:
(ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _

Premises used: Iff.mpr, LT.lt.le, measurableSet_Ioi, zero_le_one, MeasureTheory.ae_restrict_iff', Real.rpow_nonneg, LE.le.trans, Filter.EventuallyLE, Neg.neg, Filter.univ_mem'
-- 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)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioi 1))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ a ^ (-s)

Tactic:
exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _

Premises used: Iff.mpr, measurableSet_Ioi, zero_le_one, MeasureTheory.ae_restrict_iff', Real.rpow_nonneg, LE.le.trans, Filter.univ_mem'
-- 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)
rwa rwa₁ rwa₂ rwa₃ : 1 < s
⊢ -s < -1

Tactic:
rwa [neg_lt_neg_iff]

Premises used: neg_lt_neg_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)
rw : ε * ((s - 1) * (-1 / (-s + 1))) = ε
⊢ ε *
      ((s - 1) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)) =
    ε

Tactic:
rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]

Premises used: integral_Ioi_rpow_of_lt, Real.one_rpow, zero_lt_one
-- 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)
linarith : -s + 1 = 0 → 1 - s + -(-s + 1 - 0) = 0
⊢ -s + 1 ≠ 0

Tactic:
linarith
-- 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) * (-1 / (-s + 1))) = ε

Tactic:
field [show -s + 1 ≠ 0 by linarith]
-- 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)
_₁ :
  ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ε * t ^ (-s)) ≤
    ε *
      ((s - 1) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s))
_₂ :
  ε *
      ((s - 1) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)) =
    ε
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε

Tactic:
calc
    _ ≤ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ε * t ^ (-s) := by
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
      · exact (lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁
      · exact (integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) hT₀).const_mul _
      · have ht' : 0 < t := hT₀.trans ht
        rw [h ht', ← mul_assoc]
        exact mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)
    _ ≤ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) := by
      rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
      · exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one
      · exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _
    _ = ε := by
      rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
      field [show -s + 1 ≠ 0 by linarith]

Premises used: Set.Ioi, HMul.hMul, HSub.hSub, MeasureTheory.Measure.restrict, HPow.hPow, MeasureTheory.MeasureSpace.volume, MeasureTheory.integral, 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)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
obtain :
  ∀ (T : ℝ) (hT₁ : 1 ≤ T) (hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y),
    ∃ C ≥ 0,
      EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
        (s - 1) * s * C + s * ε
⊢ ∃ C ≥ 0,
    EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
      (s - 1) * s * C + s * ε

Tactic:
obtain ⟨T, hT₁, hT⟩ := (eventually_forall_ge_atTop.mpr
    (LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₁
      hlim hε)).frequently.forall_exists_of_atTop 1

Premises used: Iff.mpr, _private.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₁, Filter.Frequently.forall_exists_of_atTop, Filter.Eventually.frequently, OfNat.ofNat, Filter.eventually_forall_ge_atTop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
⊢ 0 ≤ C

Tactic:
setIntegral_nonneg_ae measurableSet_Ioc (univ_mem' fun t ht ↦ ?_)

Premises used: MeasureTheory.setIntegral_nonneg_ae, measurableSet_Ioc, Filter.univ_mem'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
refine : ∀ (t : ℝ) (ht : t ∈ Set.Ioc 1 T), 0 ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
⊢ 0 ≤ C

Tactic:
refine setIntegral_nonneg_ae measurableSet_Ioc (univ_mem' fun t ht ↦ ?_)

Premises used: MeasureTheory.setIntegral_nonneg_ae, measurableSet_Ioc, Filter.univ_mem'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ 0 ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1

Tactic:
mul_nonneg (norm_nonneg _) <| Real.rpow_nonneg (zero_le_one.trans ht.1.le) _

Premises used: mul_nonneg, LT.lt.le, zero_le_one, And.left, Real.rpow_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ 0 ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1

Tactic:
exact mul_nonneg (norm_nonneg _) <| Real.rpow_nonneg (zero_le_one.trans ht.1.le) _

Premises used: mul_nonneg, LT.lt.le, zero_le_one, And.left, Real.rpow_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
⊢ 0 ≤ C

Tactic:
have hC : 0 ≤ C := by
    refine setIntegral_nonneg_ae measurableSet_Ioc (univ_mem' fun t ht ↦ ?_)
    exact mul_nonneg (norm_nonneg _) <| Real.rpow_nonneg (zero_le_one.trans ht.1.le) _
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
⊢ ∃ C ≥ 0,
    EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
      (s - 1) * s * C + s * ε

Tactic:
⟨C, hC, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
refine :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
⊢ ∃ C ≥ 0,
    EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
      (s - 1) * s * C + s * ε

Tactic:
refine ⟨C, hC, ?_⟩
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
h :
  ∀ (s : ℝ) (hs : Membership.mem (γ := Set ℝ) (Set.Ioi 1) s),
    ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
⊢ EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε

Tactic:
filter_upwards [eventually_mem_nhdsWithin] with s hs

Premises used: eventually_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : Membership.mem (γ := Set ℝ) (Set.Ioi 1) s
⊢ 1 < s

Tactic:
rw [Set.mem_Ioi] at hs

Premises used: Set.mem_Ioi
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
⊢ 0 ≤ (s - 1) * s

Tactic:
have hs' : 0 ≤ (s - 1) * s := mul_nonneg (sub_nonneg.mpr hs.le) (zero_le_one.trans hs.le)
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ l * (↑t : ℂ)) (Set.Ici 1)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
refine : LocallyIntegrableOn S (Set.Ici 1) volume
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume

Tactic:
refine .sub ?_ <| ContinuousOn.locallyIntegrableOn (by fun_prop) measurableSet_Ici

Premises used: ContinuousOn.locallyIntegrableOn, measurableSet_Ici