∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {a : ℝ} {m : ℕ},
  0 ≤ a →
    ∀ {g : ℝ → 𝕜},
      MeasureTheory.LocallyIntegrableOn g (Set.Ici a) MeasureTheory.volume →
        MeasureTheory.LocallyIntegrableOn (fun t => g t * ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k) (Set.Ici a) MeasureTheory.volume