awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
hf _
-- 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:
exact hf _
-- 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:
tsub_le_tsub_right (le_of_eq_of_le (Real.norm_of_nonneg ?_).symm (hC₁ n)) _

Premises used: le_of_eq_of_le, tsub_le_tsub_right, Eq.symm, Real.norm_of_nonneg
-- 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 : 0 ≤ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖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‖)) ≤
    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:
refine tsub_le_tsub_right (le_of_eq_of_le (Real.norm_of_nonneg ?_).symm (hC₁ n)) _

Premises used: le_of_eq_of_le, tsub_le_tsub_right, Eq.symm, Real.norm_of_nonneg
-- 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 : ℕ
⊢ 0 ≤ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖

Tactic:
mul_nonneg (norm_nonneg _) (sum_nonneg fun _ _ ↦ norm_nonneg _)

Premises used: mul_nonneg, Finset.sum_nonneg, norm_nonneg
-- 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 : ℕ
⊢ 0 ≤ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖

Tactic:
exact mul_nonneg (norm_nonneg _) (sum_nonneg fun _ _ ↦ norm_nonneg _)

Premises used: mul_nonneg, Finset.sum_nonneg, norm_nonneg
-- 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 :
  (C₁ +
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
        fun (a : ℝ) ↦ |HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) a) (∑ k ∈ Icc 0 ⌊a⌋₊, ‖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‖)‖
⊢ (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:
grw [sub_eq_add_neg, neg_le_abs, abs_integral_le_integral_abs]

Premises used: sub_eq_add_neg, neg_le_abs, MeasureTheory.abs_integral_le_integral_abs
-- 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 (a : ℝ) ↦ |HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) a) (∑ k ∈ Icc 0 ⌊a⌋₊, ‖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:
simp
-- 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 :
  (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.Ioi (↑m : ℝ))) 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‖)‖) ≤
    C₁ + C₂

Tactic:
unfold C₂
-- 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 : ℕ
grw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) x) (∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖)‖) (Set.Ioi (↑m : ℝ))
    volume
⊢ (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.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
        ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖

Tactic:
grw [setIntegral_mono_set ?_ (.of_forall fun _ ↦ norm_nonneg _)
          Set.Ioc_subset_Ioi_self.eventuallyLE]

Premises used: MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, Filter.Eventually.of_forall, Set.Ioc_subset_Ioi_self, norm_nonneg
-- 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 : ℕ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) x) (∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖))
    (Measure.restrict volume (Set.Ici (↑m : ℝ)))

Tactic:
fun_prop
-- 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 : ℕ
rw :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) x) (∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖))
    (Measure.restrict volume (Set.Ici (↑m : ℝ)))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) x) (∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖)‖) (Set.Ioi (↑m : ℝ))
    volume

Tactic:
rw [← integrableOn_Ici_iff_integrableOn_Ioi, IntegrableOn,
          integrable_norm_iff (by fun_prop)]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_norm_iff, integrableOn_Ici_iff_integrableOn_Ioi
-- 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 : ℕ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) x) (∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖))
    (Measure.restrict volume (Set.Ici (↑m : ℝ)))

Tactic:
(locallyIntegrableOn_mul_sum_Icc _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop
          hg₁ hg₂

Premises used: Nat.cast_nonneg, MeasureTheory.IntegrableOn, locallyIntegrableOn_mul_sum_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- 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 : ℕ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) x) (∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖))
    (Measure.restrict volume (Set.Ici (↑m : ℝ)))

Tactic:
exact (locallyIntegrableOn_mul_sum_Icc _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop
          hg₁ hg₂

Premises used: Nat.cast_nonneg, locallyIntegrableOn_mul_sum_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 0) volume
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
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
rwa rwa₁ rwa₂ rwa₃ : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 0) volume
⊢ LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici (↑0 : ℝ)) volume

Tactic:
rwa [Nat.cast_zero]

Premises used: Nat.cast_zero