eLpNorm'_enorm

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNorm'_enorm

English

The eLp norm of the norm of a function equals the eLp norm of the function itself.

Русский

eLp-норма нормы функции равна eLp-норме самой функции.

LaTeX

$$$eLpNorm\bigl(\mathrm{fun}\;x\, \|f(x)\|\bigr)\; p\; μ = eLpNorm\; f\; p\; μ.$$$

Lean4

@[simp]
theorem eLpNorm'_enorm {f : α → ε} : eLpNorm' (fun a => ‖f a‖ₑ) q μ = eLpNorm' f q μ := by
  simp [eLpNorm'_eq_lintegral_enorm]

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

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

Разделы

Аффилиация

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