enorm_toLp

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.enorm_toLp

English

The edistance between the Lp-representatives of f and g equals the eLpNorm of their difference.

Русский

Расстояние по edist между представителями f и g в Lp равно eLpNorm(f−g).

LaTeX

$$edist (hf f) (hg g) = eLpNorm (f - g) p μ$$

Lean4

theorem enorm_toLp {f : α → E} (hf : MemLp f p μ) : ‖hf.toLp f‖ₑ = eLpNorm f p μ := by
  simp [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]

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

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

Разделы

Аффилиация

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