awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ ∫ (x : ℝ) in 1..(↑n : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have h : ∀ (a : ℕ) (h : 1 ≤ a),
  Eq.{u_1 + 1} (α := 𝕜) (∫ (x : ℝ) in 1..(↑a : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑a : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
Tactic: filter_upwards [eventually_ge_atTop 1] with _ h
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
a : ℕ
h : 1 ≤ a
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : ℝ) in 1..(↑a : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑a : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
have h₁ : Eq.{u_1 + 1} (α := 𝕜) (∫ (x : ℝ) in 1..(↑a : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
  (∫ (x : ℝ) in 1..(↑a : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
Tactic: rw [← integral_of_le (Nat.one_le_cast.mpr h)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f (↑k : ℝ) * c k) atTop
    (𝓝
      (l -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have h : EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ ∫ (x : ℝ) in 1..(↑n : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
  fun (n : ℕ) ↦
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
    deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: have h : (fun n : ℕ ↦ ∫ (x : ℝ) in (1 : ℝ)..n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop]
      (fun n : ℕ ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) := by
    filter_upwards [eventually_ge_atTop 1] with _ h
    rw [← integral_of_le (Nat.one_le_cast.mpr h)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ ∫ (x : ℝ) in 1..(↑n : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have refine : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
  (Set.Ioi 1) volume
Tactic: refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ ∫ (x : ℝ) in 1..(↑n : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f (↑k : ℝ) * c k) atTop
    (𝓝
      (l -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have h_lim' : Tendsto.{0, u_1} (β := 𝕜)
  (fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
  atTop
  (𝓝
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
Tactic: have h_lim' : Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (1 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
      atTop (𝓝 (∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
    refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
    exact Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c zero_le_one hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ ∫ (x : ℝ) in 1..(↑n : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f (↑k : ℝ) * c k) atTop
    (𝓝
      (l -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have refine : ∀ (x : ℕ),
  (f (↑x : ℝ) * ∑ k ∈ Icc 0 x, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑x : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    ∑ k ∈ Icc 0 x, f (↑k : ℝ) * c k
Tactic: refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : Asymptotics.IsBigO.{0, u_1, 0} (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ ∫ (x : ℝ) in 1..(↑n : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x : ℕ
⊢ (f (↑x : ℝ) * ∑ k ∈ Icc 0 x, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 (↑x : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    ∑ k ∈ Icc 0 x, f (↑k : ℝ) * c k
have rw : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 (↑x : ℝ)) volume
Tactic: rw [sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑m : ℝ)) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n
have obtain : ∀ (C₁ : ℝ) (hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁),
  Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n
Tactic: obtain ⟨C₁, hC₁⟩ := Asymptotics.isBigO_one_nat_atTop_iff.mp h_bdd
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑m : ℝ)) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
    ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n
have refine : ∀ (n : ℕ), ∑ i ∈ range n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
Tactic: refine summable_of_sum_range_norm_le (c := max (C₁ + C₂) 1) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑m : ℝ)) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
    ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
n : ℕ
⊢ ∑ i ∈ range (n + 1), ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
have succ : ∑ i ∈ Icc 0 n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
Tactic: rw [Nat.range_eq_Icc_zero_sub_one _ n.add_one_ne_zero, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑m : ℝ)) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
    ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
n : ℕ
⊢ ∑ i ∈ Icc 0 n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
have succ : ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
  ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ))) fun (t : ℝ) ↦
      HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
Tactic: calc
        _ = ∑ k ∈ Icc 0 n, ‖f k‖ * ‖c k‖ := by simp_rw [norm_mul]
        _ = ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
              ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ - ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ + ∫ t in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ := ?_
        _ ≤ C₁ + C₂ := ?_
        _ ≤ max (C₁ + C₂) 1 := le_max_left _ _
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑m : ℝ)) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
    ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
n : ℕ
succ :
  ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
    ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
⊢ ∑ i ∈ Icc 0 n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
have succ₁ : (‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ))) fun (t : ℝ) ↦
      HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) ≤
  C₁ -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ))) fun (t : ℝ) ↦
      HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
Tactic: calc
        _ = ∑ k ∈ Icc 0 n, ‖f k‖ * ‖c k‖ := by simp_rw [norm_mul]
        _ = ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
              ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ - ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ + ∫ t in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ := ?_
        _ ≤ C₁ + C₂ := ?_
        _ ≤ max (C₁ + C₂) 1 := le_max_left _ _
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑m : ℝ)) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
    ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
n : ℕ
succ :
  ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖ =
    ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
succ₁ :
  (‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) ≤
    C₁ -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
⊢ ∑ i ∈ Icc 0 n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
have succ₂ : (C₁ -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ))) fun (t : ℝ) ↦
      HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) ≤
  C₁ +
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ))) fun (t : ℝ) ↦
      ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
Tactic: calc
        _ = ∑ k ∈ Icc 0 n, ‖f k‖ * ‖c k‖ := by simp_rw [norm_mul]
        _ = ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
              ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ - ∫ t in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ := ?_
        _ ≤ C₁ + ∫ t in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ := ?_
        _ ≤ C₁ + C₂ := ?_
        _ ≤ max (C₁ + C₂) 1 := le_max_left _ _