memLp_finset_sum'

Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

URI: https://scilib.ai/kg/mathlib#MeasureTheory.memLp_finset_sum'

← MathLib Explorer

English

Same as above: the finite sum of MemLp functions is MemLp.

Русский

То же самое: конечная сумма функций MemLp принадлежит MemLp.

LaTeX

$$MemLp (∑ i ∈ s, f i) p μ$$

Lean4

theorem memLp_finset_sum' [ContinuousAdd ε'] {ι} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
    MemLp (∑ i ∈ s, f i) p μ := by
  convert memLp_finset_sum s hf using 1
  ext x
  simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru