English
If g is locally integrable on [a, ∞) and m is fixed, then the product g(t) times the finite forward sum over k ≤ ⌊t⌋ is locally integrable on [a, ∞).
Русский
Если g локально интегрируема на [a, ∞) и фиксировано m, то произведение g(t) на скобочную сумму по k ≤ ⌊t⌋ остаётся локально интегрируемым на [a, ∞).
LaTeX
$$$\\text{LocallyIntegrableOn }\\left(g(t) \\sum_{k \\in Icc m \\!\\left( \\lfloor t \\rfloor \\right)_+} c(k) \\right)\\; (\\text{Ici } a)$$$
Lean4
theorem locallyIntegrableOn_mul_sum_Icc {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜} (hg : LocallyIntegrableOn g (Set.Ici a)) :
LocallyIntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Ici a) :=
by
refine (locallyIntegrableOn_iff isLocallyClosed_Ici).mpr fun K hK₁ hK₂ ↦ ?_
by_cases hK₃ : K.Nonempty
· have h_inf : a ≤ sInf K := (hK₁ (hK₂.sInf_mem hK₃))
refine IntegrableOn.mono_set ?_ (Bornology.IsBounded.subset_Icc_sInf_sSup hK₂.isBounded)
refine integrableOn_mul_sum_Icc _ (ha.trans h_inf) ?_
refine hg.integrableOn_compact_subset ?_ isCompact_Icc
exact (Set.Icc_subset_Ici_iff (Real.sInf_le_sSup _ hK₂.bddBelow hK₂.bddAbove)).mpr h_inf
· rw [Set.not_nonempty_iff_eq_empty.mp hK₃]
exact integrableOn_empty
