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 : 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)
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)
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 _)]
-- 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 *
      (Cs +
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
          ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
have hfs : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
  (Set.Ioc 1 T) volume
Tactic: rw [← Set.Ioc_union_Ioi_eq_Ioi hT₁, setIntegral_union Set.Ioc_disjoint_Ioi_same
        measurableSet_Ioi]
-- 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
hfs :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ioc 1 T) volume
⊢ ((s - 1) * s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) =
    (s - 1) * s *
      (Cs +
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
          ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
have hft : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
  (Set.Ioi T) volume
Tactic: rw [← Set.Ioc_union_Ioi_eq_Ioi hT₁, setIntegral_union Set.Ioc_disjoint_Ioi_same
        measurableSet_Ioi]
-- 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 *
      (Cs +
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
          ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) * s * C +
      s *
        ((s - 1) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
            ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
have rw : ((s - 1) * s * Cs +
    (s - 1) * s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
  (s - 1) * s * C +
    (s - 1) * s *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
Tactic: rw [mul_add, ← mul_assoc, mul_comm s]
-- 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 * C +
      s *
        ((s - 1) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
            ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    (s - 1) * s * C + s * ε
have bc : ((s - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
      ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
  ε
Tactic: gcongr
-- 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 : ℂ)
C ε : ℝ
⊢ 𝓝 ε = 𝓝 (HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε)
have e_x : ε = HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε
Tactic: congr
-- 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 : ℂ)
C ε : ℝ
⊢ Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
have rw : Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 (HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε))
Tactic: rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
-- 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 : ℂ)
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 l)
have h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
Tactic: have h₁ {C ε : ℝ} : Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε) := by
    rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
    exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
have obtain : ∀ C ≥ 0,
  ∀
    (hC₂ :
      EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
        (s - 1) * s * C + s * 1),
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦
      ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
Tactic: obtain ⟨C, _, hC₂⟩ :=
      LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 l)
have h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
Tactic: have h₂ : IsBoundedUnder
      (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s : ℝ ↦ ‖(s - 1) * LSeries f s - s * l‖ := by
    obtain ⟨C, _, hC₂⟩ :=
      LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
    exact h₁.isBoundedUnder_le.mono_le 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ 𝓝 l = 𝓝 (0 + 1 * l)
have e_x : l = 0 + 1 * l
Tactic: congr
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 l)
have rw : Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 (0 + 1 * l))
Tactic: rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 (0 + 1 * l))
have h₃ : Tendsto (fun (s : ℝ) ↦ (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 (1 * l))
Tactic: have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 l)
have suffices : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
Tactic: suffices Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s - s * l) (𝓝[>] 1) (𝓝 0) by
    rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
    have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
    exact (this.add h₃).congr fun _ ↦ by ring
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
have refine_1 : LE.le (α := ℝ) 0 (liminf (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1))
Tactic: refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
refine_1 : LE.le (α := ℝ) 0 (liminf (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1))
⊢ Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
have refine_2 : LE.le (α := ℝ) (limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1)) 0
Tactic: refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
refine_1 : LE.le (α := ℝ) 0 (liminf (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1))
refine_2 : LE.le (α := ℝ) (limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1)) 0
⊢ Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
have refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝[>] 1) fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖
Tactic: refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ LE.le (α := ℝ) (limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1)) 0
have refine_2 : ∀ (ε : ℝ) (hε : 0 < ε), limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ 0 + ε
Tactic: refine le_of_forall_pos_le_add fun ε hε ↦ ?_
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ 0 + ε
have refine_2 : limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε
Tactic: rw [zero_add]
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε
have refine_2 : ∀ (C : ℝ) (hC₁ : C ≥ 0)
  (hC₂ :
    EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
      (s - 1) * s * C + s * ε),
  limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε
Tactic: obtain ⟨C, hC₁, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS hε
-- 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₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε
have refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖
Tactic: refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq