English
Definition of a linear map to an Lp space from the dual, which equals MemLp.toLp when id ∈ MemLp and is zero otherwise.
Русский
Определение линейного отображения в пространство Lp из двойственного пространства, которое равно MemLp.toLp при id ∈ MemLp и равно нулю в противном случае.
LaTeX
$$$\\text{toLp}_\\ell(\\mu, p): \\text{StrongDual } 𝕜 E \\to_L[𝕜] \\mathrm{Lp}_{𝕜} p μ \\quad\\text{(definition)}$$$
Lean4
/-- Linear map from the dual to `Lp` equal to `MemLp.toLp` if `MemLp id p μ` and to 0 otherwise. -/
noncomputable def toLpₗ (μ : Measure E) (p : ℝ≥0∞) : StrongDual 𝕜 E →ₗ[𝕜] Lp 𝕜 p μ :=
if h_Lp : MemLp id p μ then
{ toFun := fun L ↦ MemLp.toLp L (h_Lp.continuousLinearMap_comp L)
map_add' u v := by push_cast; rw [MemLp.toLp_add]
map_smul' c L := by push_cast; rw [MemLp.toLp_const_smul]; rfl }
else 0
