English
For f in Lp, restricting to a set s defines a continuous linear map from Lp to Lp(μ.restrict s). Moreover, this map preserves linear structure and scalar multiplication.
Русский
Для f в Lp ограничение на множество s задает непрерывный линейный отображение из Lp в Lp(μ.restrict s); отображение сохраняет линейность и умножение на скаляр.
LaTeX
$$$$LpToLpRestrictCLM: Lp F p μ \\to Lp F p (μ|_s)$$ is a continuous linear map.$$
Lean4
/-- 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. -/
theorem Lp_toLp_restrict_add (f g : Lp E p μ) (s : Set X) :
((Lp.memLp (f + g)).restrict s).toLp (⇑(f + g)) =
((Lp.memLp f).restrict s).toLp f + ((Lp.memLp g).restrict s).toLp g :=
by
ext1
refine (ae_restrict_of_ae (Lp.coeFn_add f g)).mp ?_
refine (Lp.coeFn_add (MemLp.toLp f ((Lp.memLp f).restrict s)) (MemLp.toLp g ((Lp.memLp g).restrict s))).mp ?_
refine (MemLp.coeFn_toLp ((Lp.memLp f).restrict s)).mp ?_
refine (MemLp.coeFn_toLp ((Lp.memLp g).restrict s)).mp ?_
refine (MemLp.coeFn_toLp ((Lp.memLp (f + g)).restrict s)).mono fun x hx1 hx2 hx3 hx4 hx5 => ?_
rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]
