coeFn_toLp

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.coeFn_toLp

English

If f is AEStronglyMeasurable with respect to μ, then replacing f by its AEEqFun.mk representation does not change its eLpNorm.

Русский

При замене f на представление AEEqFun.mk (при измеримости), eLpNorm не меняется.

LaTeX

$$eLpNorm (AEEqFun.mk f hf) p μ = eLpNorm f p μ$$

Lean4

theorem coeFn_toLp {f : α → E} (hf : MemLp f p μ) : hf.toLp f =ᵐ[μ] f :=
  AEEqFun.coeFn_mk _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru