awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
refine :
  Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ) ↦ ∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) 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 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
refine Tendsto.congr (fun _ ↦ by rw [← integral_of_le (Nat.cast_nonneg _)]) ?_

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ) ↦ ∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_natCast_atTop_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 t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
refine :
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (Set.Ioi 0) volume
⊢ Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ) ↦ ∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
refine intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_natCast_atTop_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 t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (Set.Ioi 0) volume

Tactic:
Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int

Premises used: le_rfl, locallyIntegrableOn_mul_sum_Icc, integrableOn_Ici_iff_integrableOn_Ioi, Iff.mp, 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 t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (Set.Ioi 0) volume

Tactic:
exact Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int

Premises used: le_rfl, locallyIntegrableOn_mul_sum_Icc, integrableOn_Ici_iff_integrableOn_Ioi, Iff.mp, 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 t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
have h_lim' : Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (0 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
      atTop (𝓝 (∫ t in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
    refine Tendsto.congr (fun _ ↦ by rw [← integral_of_le (Nat.cast_nonneg _)]) ?_
    refine intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop
    exact Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) 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 0)) 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 : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) 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 0 (↑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 0)) 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 : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x : ℕ
rw : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑x : ℝ)) volume
⊢ (f (↑x : ℝ) * ∑ k ∈ Icc 0 x, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑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' _ _ (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 : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x : ℕ
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑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 : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x : ℕ
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑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 : ℝ → 𝕜
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 :
  ∀ (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)
⊢ 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:
filter_upwards [eventually_ge_atTop 1] with _ h

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- 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
a : ℕ
h : 1 ≤ a
h₁ 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)
⊢ 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:
rw [← integral_of_le (Nat.one_le_cast.mpr h)]

Premises used: Iff.mpr, Nat.one_le_cast, intervalIntegral.integral_of_le
-- 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
⊢ 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)]
-- 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
⊢ 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:
Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_natCast_atTop_atTop, Filter.Tendsto.congr'
-- 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
refine :
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (Set.Ioi 1) volume
⊢ 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:
refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_natCast_atTop_atTop, Filter.Tendsto.congr'
-- 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
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (Set.Ioi 1) volume

Tactic:
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

Premises used: zero_le_one, locallyIntegrableOn_mul_sum_Icc, integrableOn_Ici_iff_integrableOn_Ioi, Iff.mp, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- 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
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (Set.Ioi 1) volume

Tactic:
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

Premises used: zero_le_one, locallyIntegrableOn_mul_sum_Icc, integrableOn_Ici_iff_integrableOn_Ioi, Iff.mp, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop
-- 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
⊢ 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