locallyIntegrable_finset_sum — Mathlib

English

If each f_i is locally integrable for i in a finite index set, then the finite sum over i of f_i is locally integrable.

Русский

Если каждый f_i локально интегрируем для i в конечном множестве индексов, то сумма по i от f_i локально интегрируема.

LaTeX

$$$\forall i\, i\in s \implies \operatorname{LocallyIntegrable}(f_i, \mu) \Rightarrow \operatorname{LocallyIntegrable}\left( a \mapsto \sum_{i\in s} f_i(a) \right, \mu\right)$$$

Lean4

theorem locallyIntegrable_finset_sum {ι} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) :
    LocallyIntegrable (fun a ↦ ∑ i ∈ s, f i a) μ := by
  simpa only [← Finset.sum_apply] using locallyIntegrable_finset_sum' s hf

Похожие утверждения