eLpNorm'_measure_zero_of_neg

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

Negating the function does not change the eLpNorm' value: eLpNorm'(-f) q μ = eLpNorm'(f) q μ.

Русский

Отрицание функции не изменяет значение eLpNorm': eLpNorm'(-f) q μ = eLpNorm'(f) q μ.

LaTeX

$$$eLpNorm'(-f)\\, q \\,\\mu = eLpNorm'(f)\\, q \\,\\mu$$$

Lean4

theorem eLpNorm'_measure_zero_of_neg {f : α → ε} (hq_neg : q < 0) : eLpNorm' f q (0 : Measure α) = ∞ := by
  simp [eLpNorm', hq_neg]

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

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

Разделы

Аффилиация

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