awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.AbelSummation
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))

Tactic:
(h_lim.sub h_lim').congr (fun _ ↦ ?_)

Premises used: Filter.Tendsto.congr, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.AbelSummation
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))
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
⊢ 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))

Tactic:
refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)

Premises used: Filter.Tendsto.congr, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
rw : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 (↑x : ℝ)) volume
⊢ (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:
rw [sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)]

Premises used: sum_mul_eq_sub_integral_mul₀', And.left
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 (↑x : ℝ)) volume

Tactic:
hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, Set.Icc_subset_Ici_self
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 (↑x : ℝ)) volume

Tactic:
exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, Set.Icc_subset_Ici_self
-- Module: Mathlib.NumberTheory.AbelSummation
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
obtain :
  ∀ (C₁ : ℝ) (hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁),
    Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n

Tactic:
obtain ⟨C₁, hC₁⟩ := Asymptotics.isBigO_one_nat_atTop_iff.mp h_bdd

Premises used: Asymptotics.isBigO_one_nat_atTop_iff, Iff.mp
-- Module: Mathlib.NumberTheory.AbelSummation
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

Tactic:
summable_of_sum_range_norm_le (c := max (C₁ + C₂) 1) fun n ↦ ?_

Premises used: summable_of_sum_range_norm_le
-- Module: Mathlib.NumberTheory.AbelSummation
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‖)‖
refine : ∀ (n : ℕ), ∑ i ∈ range n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n

Tactic:
refine summable_of_sum_range_norm_le (c := max (C₁ + C₂) 1) fun n ↦ ?_

Premises used: summable_of_sum_range_norm_le
-- Module: Mathlib.NumberTheory.AbelSummation
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‖)‖
⊢ ∑ i ∈ range 0, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1

Tactic:
simp only [range_zero, norm_mul, sum_empty, le_sup_iff, zero_le_one, or_true]

Premises used: norm_mul, zero_le_one, le_sup_iff, Finset.sum_empty, or_true, Finset.range_zero
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ∑ i ∈ Icc 0 n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
⊢ ∑ i ∈ range (n + 1), ‖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]

Premises used: Nat.add_one_ne_zero, Nat.range_eq_Icc_zero_sub_one, add_tsub_cancel_right
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ Eq (α := ℝ) (∑ i ∈ Icc 0 n, ‖f (↑i : ℝ) * c i‖) (∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * ‖c k‖)

Tactic:
simp_rw [norm_mul]

Premises used: norm_mul
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ ∑ 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:
?_
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ (‖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:
?_
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ (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:
?_
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ (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₁ + C₂

Tactic:
?_
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
⊢ C₁ + C₂ ≤ max (C₁ + C₂) 1

Tactic:
le_max_left _ _

Premises used: le_max_left