lpTrimToLpMeas — Mathlib

English

There is an inverse map from Lp(μ.trim hm) to lpMeas on μ, sending an Lp function to its lpMeas representation.

Русский

Существует обратное отображение из Lp(μ.trim hm) в lpMeas на μ, переводя функцию Lp в представление lpMeas.

LaTeX

$$$\text{lpTrimToLpMeas}(hm,f) : lpMeas F m p μ$$$

Lean4

/-- Map from `Lp F p (μ.trim hm)` to `lpMeas`, inverse of `Lp_meas_to_Lp_trim`. -/
noncomputable def lpTrimToLpMeas (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) : lpMeas F 𝕜 m p μ :=
  ⟨(memLp_of_memLp_trim hm (Lp.memLp f)).toLp f, mem_lpMeasSubgroup_toLp_of_trim hm f⟩

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