∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  c 0 = 0 →
    (∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t) →
      MeasureTheory.LocallyIntegrableOn (deriv f) (Set.Ici 1) MeasureTheory.volume →
        ∀ {l : 𝕜},
          Filter.Tendsto (fun n => f ↑n * ∑ k ∈ Finset.Icc 0 n, c k) Filter.atTop (nhds l) →
            ∀ {g : ℝ → ℝ},
              (fun t => deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k) =O[Filter.atTop] g →
                MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume →
                  Filter.Tendsto (fun n => ∑ k ∈ Finset.Icc 0 n, f ↑k * c k) Filter.atTop
                    (nhds (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k))