awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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 T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε
have _₂ : ε *
    ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦ t ^ (-s)) =
  ε
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
⊢ ∃ C ≥ 0,
    EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
      (s - 1) * s * C + s * ε
have 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 * ε
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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
have refine : ∀ (t : ℝ) (ht : t ∈ Set.Ioc 1 T), 0 ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
Tactic: refine setIntegral_nonneg_ae measurableSet_Ioc (univ_mem' fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
⊢ ∃ C ≥ 0,
    EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
      (s - 1) * s * C + s * ε
have hC : 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) _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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 * ε
have refine : EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
  (s - 1) * s * C + s * ε
Tactic: refine ⟨C, hC, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
⊢ EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
have h : ∀ (s : ℝ) (hs : Membership.mem (γ := Set ℝ) (Set.Ioi 1) s),
  ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
Tactic: filter_upwards [eventually_mem_nhdsWithin] with s hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
⊢ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
have hs₁ : 1 < s
Tactic: rw [Set.mem_Ioi] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
⊢ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
have hs' : 0 ≤ (s - 1) * s
Tactic: have hs' : 0 ≤ (s - 1) * s := mul_nonneg (sub_nonneg.mpr hs.le) (zero_le_one.trans hs.le)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
⊢ LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
have refine : LocallyIntegrableOn S (Set.Ici 1) volume
Tactic: refine .sub ?_ <| ContinuousOn.locallyIntegrableOn (by fun_prop) measurableSet_Ici
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
⊢ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
have h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
Tactic: have h₀ : LocallyIntegrableOn (fun t ↦ S t - l * t) (Set.Ici 1) := by
    refine .sub ?_ <| ContinuousOn.locallyIntegrableOn (by fun_prop) measurableSet_Ici
    simpa using locallyIntegrableOn_mul_sum_Icc f zero_le_one (locallyIntegrableOn_const 1)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
⊢ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
have h₁ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
  (Set.Ici 1) volume
Tactic: have h₁ : IntegrableOn (fun t ↦ ‖S t - l * t‖ * t ^ (-s - 1)) (Set.Ici 1) :=
    lemma₂ hs h₀ fun t ht ↦ (hT t ht).le
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
have refine : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ici 1)
Tactic: refine ((h₀.norm.mul_continuousOn ?_ isLocallyClosed_Ici).integrableOn_compact_subset
      Set.Icc_subset_Ici_self isCompact_Icc).mono_set Set.Ioc_subset_Icc_self
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
⊢ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
have h₂ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
Tactic: have h₂ : IntegrableOn (fun t : ℝ ↦ ‖S t - l * t‖ * (t ^ ((-1 : ℝ) - 1))) (Set.Ioc 1 T) := by
    refine ((h₀.norm.mul_continuousOn ?_ isLocallyClosed_Ici).integrableOn_compact_subset
      Set.Icc_subset_Ici_self isCompact_Icc).mono_set Set.Ioc_subset_Icc_self
    exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ (-(↑s : ℂ)).re < -1
have rwa : -(↑s : ℂ).re < -1
Tactic: rwa [neg_re, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
rwa : -(↑s : ℂ).re < -1
⊢ (-(↑s : ℂ)).re < -1
have rwa₁ : 1 < (↑s : ℂ).re
Tactic: rwa [neg_re, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
have hb : (↑s : ℂ) - 1 ≠ 0
Tactic: rw [integral_Ioi_cpow_of_lt (by rwa [neg_re, neg_lt_neg_iff]) zero_lt_one, ofReal_one,
      one_cpow, show -(s : ℂ) + 1 = -(s - 1) by ring, neg_div_neg_eq, mul_div_cancel₀]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (hypothesis)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
⊢ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖ ≤ (s - 1) * s * C + s * ε
have h₃ : (((↑s : ℂ) - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (-(↑s : ℂ))) =
  1
Tactic: have h₃ : (s - 1) * ∫ (t : ℝ) in Set.Ioi 1, (t : ℂ) ^ (-s : ℂ) = 1 := by
    rw [integral_Ioi_cpow_of_lt (by rwa [neg_re, neg_lt_neg_iff]) zero_lt_one, ofReal_one,
      one_cpow, show -(s : ℂ) + 1 = -(s - 1) by ring, neg_div_neg_eq, mul_div_cancel₀]
    exact (sub_ne_zero.trans ofReal_ne_one).mpr hs.ne'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
⊢ Cs ≤ C
have refine_1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
  (Set.Ioc 1 T) volume
Tactic: refine setIntegral_mono_on ?_ h₂ measurableSet_Ioc fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
refine_1 :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioc 1 T) volume
⊢ Cs ≤ C
have refine_2 : ∀ (t : ℝ) (ht : t ∈ Set.Ioc 1 T),
  ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
Tactic: refine setIntegral_mono_on ?_ h₂ measurableSet_Ioc fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.SumCoeff (goal)
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
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1) ≤ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
have refine_2 : 1 ≤ t
Tactic: gcongr