English
Finite sums of interval-integrable functions are interval-integrable (alternate formulation with finsum).
Русский
Конечные суммы интервал-интегрируемых функций остаются интервал-интегрируемыми (альтернативная формулировка с finsum).
LaTeX
$$$\operatorname{IntervalIntegrable}(\text{finsum } f_i,\mu,a,b)$$$
Lean4
/-- Finite sums of interval integrable functions are interval integrable. -/
@[simp]
protected theorem finsum {ε} [TopologicalSpace ε] [ENormedAddCommMonoid ε] [ContinuousAdd ε] [PseudoMetrizableSpace ε]
{f : ι → ℝ → ε} (h : ∀ i, IntervalIntegrable (f i) μ a b) : IntervalIntegrable (∑ᶠ i, f i) μ a b :=
by
by_cases h₁ : f.support.Finite
· simp [finsum_eq_sum _ h₁, IntervalIntegrable.sum h₁.toFinset (fun i _ ↦ h i)]
· rw [finsum_of_infinite_support h₁]
apply intervalIntegrable_const_iff (c := 0) (by simp) |>.2
tauto
