awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h₄ : Cs ≤ C
t : ℝ
ht : (↑t : ℂ) ≠ 0
⊢ S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) = (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
have e_a : S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
  S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
Tactic: rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ 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)
h₄ : Cs ≤ C
t : ℝ
ht : (↑t : ℂ) ≠ 0
e_a :
  S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
⊢ S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) = (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
have e_a₁ : S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) -
    l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1)
Tactic: rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ 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)
h₄ : Cs ≤ C
t : ℝ
ht : (↑t : ℂ) ≠ 0
e_a :
  S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
e_a₁ :
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) -
      l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1)
⊢ S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) = (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
have e_a₂ : S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ))
Tactic: rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ 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)
h₄ : Cs ≤ C
t : ℝ
ht : (↑t : ℂ) ≠ 0
e_a :
  S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
e_a₁ :
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) -
      l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1)
e_a₂ :
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ))
⊢ S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) = (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
have e_a₃ : S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * ((↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)))
Tactic: rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ 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)
h₄ : Cs ≤ C
t : ℝ
ht : (↑t : ℂ) ≠ 0
e_a :
  S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
e_a₁ :
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1) -
      l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / HPow.hPow (β := ℂ) (↑t : ℂ) 1)
e_a₂ :
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ))
e_a₃ :
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
    S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * ((↑t : ℂ) * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)))
⊢ S t * (↑t : ℂ) ^ (-(↑s : ℂ) - 1) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) = (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)
have e_a₄ : S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ)) =
  S t * ((↑t : ℂ) ^ (-(↑s : ℂ)) / (↑t : ℂ)) - l * (↑t : ℂ) ^ (-(↑s : ℂ))
Tactic: rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ 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)
h₄ : Cs ≤ C
⊢ ‖((↑s : ℂ) - 1) * (↑s : ℂ) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
          (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ ≤
    (s - 1) * s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖
have rw : (s - 1) * s *
    norm (E := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)) ≤
  (s - 1) * s *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖
Tactic: rw [norm_mul, show ((s : ℂ) - 1) * s = ((s - 1) * s : ℝ) by simp, norm_real,
        Real.norm_of_nonneg hs']
-- 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)
h₄ : Cs ≤ C
⊢ ((s - 1) * s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖) =
    (s - 1) * s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
have e_a : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
    ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
Tactic: congr 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
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)
h₄ : Cs ≤ C
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
have e_a : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Ioi 1) t),
  ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi 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
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)
h₄ : Cs ≤ C
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Ioi 1) t
⊢ ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
have ht₁ : 0 ≤ t
Tactic: replace ht : 0 ≤ t := zero_le_one.trans ht.le
Cleared hypotheses: 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)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
⊢ ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
have e_a : ‖S t - l * (↑t : ℂ)‖ * ‖(↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
Tactic: rw [norm_mul, show (-(s : ℂ) - 1) = (-s - 1 : ℝ) by simp, ← ofReal_cpow ht, norm_real,
        Real.norm_of_nonneg (Real.rpow_nonneg 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)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
e_a : ‖S t - l * (↑t : ℂ)‖ * ‖(↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
⊢ ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
have e_a₁ : ‖S t - l * (↑t : ℂ)‖ * ‖(↑t : ℂ) ^ (↑(-s - 1) : ℂ)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
Tactic: rw [norm_mul, show (-(s : ℂ) - 1) = (-s - 1 : ℝ) by simp, ← ofReal_cpow ht, norm_real,
        Real.norm_of_nonneg (Real.rpow_nonneg 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)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
e_a : ‖S t - l * (↑t : ℂ)‖ * ‖(↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
e_a₁ : ‖S t - l * (↑t : ℂ)‖ * ‖(↑t : ℂ) ^ (↑(-s - 1) : ℂ)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
⊢ ‖(S t - l * (↑t : ℂ)) * (↑t : ℂ) ^ (-(↑s : ℂ) - 1)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
have e_a₂ : ‖S t - l * (↑t : ℂ)‖ * ‖(↑(t ^ (-s - 1)) : ℂ)‖ = ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
Tactic: rw [norm_mul, show (-(s : ℂ) - 1) = (-s - 1 : ℝ) by simp, ← ofReal_cpow ht, norm_real,
        Real.norm_of_nonneg (Real.rpow_nonneg ht _)]