toLp — Mathlib

English

The equality of the coefficients between a bounded continuous function and its Lp representative is valid almost everywhere.

Русский

Справедливо равенство коэффициентов между ограниченной непрерывной функцией и её представлением в Lp (почти всюду).

LaTeX

$$$(f: BoundedContinuousFunction) \\toLp(p,μ) = f \\;\\text{a.e.}$$$

Lean4

/-- The bounded linear map of considering a bounded continuous function on a finite-measure space
as an element of `Lp`. -/
noncomputable def toLp : (α →ᵇ E) →L[𝕜] Lp E p μ :=
  LinearMap.mkContinuous
    (LinearMap.codRestrict (Lp.LpSubmodule 𝕜 E p μ)
      ((ContinuousMap.toAEEqFunLinearMap μ).comp (toContinuousMapLinearMap α E 𝕜)) mem_Lp)
    _ Lp_norm_le

Похожие утверждения