English
The Lp restriction operator is a continuous linear map (CLM) between Lp spaces, compatible with scalar multiplication.
Русский
Оператор ограничения Lp является непрерывно-линейным отображением между пространствами Lp и совместим со скалярами.
LaTeX
$$$$LpToLpRestrictCLM: Lp F p μ →L[𝕜] Lp F p (μ.restrict s)$$$$
Lean4
/-- Continuous linear map sending a function of `Lp F p μ` to the same function in
`Lp F p (μ.restrict s)`. -/
noncomputable def LpToLpRestrictCLM (μ : Measure X) (p : ℝ≥0∞) [hp : Fact (1 ≤ p)] (s : Set X) :
Lp F p μ →L[𝕜] Lp F p (μ.restrict s) :=
@LinearMap.mkContinuous 𝕜 𝕜 (Lp F p μ) (Lp F p (μ.restrict s)) _ _ _ _ _ _ (RingHom.id 𝕜)
⟨⟨fun f => MemLp.toLp f ((Lp.memLp f).restrict s), fun f g => Lp_toLp_restrict_add f g s⟩, fun c f =>
Lp_toLp_restrict_smul c f s⟩
1 (by intro f; rw [one_mul]; exact norm_Lp_toLp_restrict_le s f)
