English
If f ∈ Lp and you restrict to s, the corresponding coeFn agrees almost everywhere with the restriction of f.
Русский
Если f ∈ Lp и ограничить на s, соответствующая функция-коэффициент совпадает почти повсюду с ограниченной функцией f.
LaTeX
$$$$\\text{ae}_{μ|_s}(f) = \\text{(restrict }s\\text{) toLp } f$$$$
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 commutes with scalar multiplication. -/
theorem Lp_toLp_restrict_smul (c : 𝕜) (f : Lp F p μ) (s : Set X) :
((Lp.memLp (c • f)).restrict s).toLp (⇑(c • f)) = c • ((Lp.memLp f).restrict s).toLp f :=
by
ext1
refine (ae_restrict_of_ae (Lp.coeFn_smul c f)).mp ?_
refine (MemLp.coeFn_toLp ((Lp.memLp f).restrict s)).mp ?_
refine (MemLp.coeFn_toLp ((Lp.memLp (c • f)).restrict s)).mp ?_
refine (Lp.coeFn_smul c (MemLp.toLp f ((Lp.memLp f).restrict s))).mono fun x hx1 hx2 hx3 hx4 => ?_
simp only [hx2, hx1, hx3, hx4, Pi.smul_apply]
