Theorems · Theorem · measure theory

MeasureTheory.Lp_toLp_restrict_add

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (f g : ↥(MeasureTheory.Lp E p μ)) (s : Set X),
  MeasureTheory.MemLp.toLp ↑↑(f + g) ⋯ = MeasureTheory.MemLp.toLp ↑↑f ⋯ + MeasureTheory.MemLp.toLp ↑↑g ⋯

For f : Lp E p μ, we can define an element of Lp E p (μ.restrict s) by (Lp.memLp f).restrict s).toLp f. This map is additive.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

0 results in Mathlib

Foundations

Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup