English
For a finite index set ι and measurable functions f_i, the eLpNorm' of their finite sum is bounded by the sum of the eLpNorm' of each summand, provided q ≥ 1.
Русский
Пусть ι — конечный индекс, f_i измеримы; тогда eLpNorm' суммы f_i не превышает суммы eLpNorm'(f_i), если q ≥ 1.
LaTeX
$$∀ s : Finset ι, (∀ i ∈ s, AEStronglyMeasurable (f i) μ) → 1 ≤ q → eLpNorm'(∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, eLpNorm'(f i) q μ$$
Lean4
theorem eLpNorm'_sum_le [ContinuousAdd ε'] {ι} {f : ι → α → ε'} {s : Finset ι}
(hfs : ∀ i, i ∈ s → AEStronglyMeasurable (f i) μ) (hq1 : 1 ≤ q) :
eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, eLpNorm' (f i) q μ :=
Finset.le_sum_of_subadditive_on_pred (fun f : α → ε' => eLpNorm' f q μ) (fun f => AEStronglyMeasurable f μ)
(eLpNorm'_zero (zero_lt_one.trans_le hq1)) (fun _f _g hf hg => eLpNorm'_add_le hf hg hq1)
(fun _f _g hf hg => hf.add hg) _ hfs
