English
Let ι be any index set, s a Finset, and f_i measurable. Then the eLp-norm of the sum over i ∈ s is bounded by the sum of eLp-norms of each f_i, assuming 1 ≤ p.
Русский
Пусть I — множество индексов, s — конечный набор, и f_i измеримы. Тогда eLpNorm суммы ∑_{i∈s} f_i не превышает сумму eLpNorm(f_i), при условии 1 ≤ p.
LaTeX
$$∀ s : Finset ι, (∀ i ∈ s, AEStronglyMeasurable (f i) μ) → 1 ≤ p → eLpNorm(∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, eLpNorm(f i) p μ$$
Lean4
theorem eLpNorm_sum_le [ContinuousAdd ε'] {ι} {f : ι → α → ε'} {s : Finset ι}
(hfs : ∀ i, i ∈ s → AEStronglyMeasurable (f i) μ) (hp1 : 1 ≤ p) :
eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, eLpNorm (f i) p μ :=
Finset.le_sum_of_subadditive_on_pred (fun f : α → ε' => eLpNorm f p μ) (fun f => AEStronglyMeasurable f μ)
eLpNorm_zero (fun _f _g hf hg => eLpNorm_add_le hf hg hp1) (fun _f _g hf hg => hf.add hg) _ hfs
