English
The a.e. equality for continuous maps transfers to Lp representations via toLp.
Русский
По Lp-представлению отображение сохраняет почти всюду равенство функции.
LaTeX
$$$(f: C(X,E)) \\Rightarrow toLp(p,μ)\\, f =^{\\mathrm{a.e.}} f$.$$
Lean4
/-- The bounded linear map of considering a continuous function on a compact finite-measure
space `α` as an element of `Lp`. By definition, the norm on `C(α, E)` is the sup-norm, transferred
from the space `α →ᵇ E` of bounded continuous functions, so this construction is just a matter of
transferring the structure from `BoundedContinuousFunction.toLp` along the isometry. -/
noncomputable def toLp : C(α, E) →L[𝕜] Lp E p μ :=
(BoundedContinuousFunction.toLp p μ 𝕜).comp
(linearIsometryBoundedOfCompact α E 𝕜).toLinearIsometry.toContinuousLinearMap
