add — Mathlib

English

If f and g are MemLp with exponent p with respect to μ, then f + g is MemLp with the same p and μ, under the assumption of continuous addition in the target space.

Русский

Пусть f и g принадлежат MemLp с экспонентой p по μ; тогда f + g принадлежит MemLp с той же самой p и μ, при условии непрерывного сложения в целевом пространстве.

LaTeX

$$(hf : MemLp f p μ) → (hg : MemLp g p μ) → MemLp (f + g) p μ$$

Lean4

theorem add [ContinuousAdd ε] (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f + g) p μ :=
  ⟨AEStronglyMeasurable.add hf.1 hg.1, eLpNorm_add_lt_top hf hg⟩

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