eLpNorm'_neg

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

In general, negation does not affect the eLpNorm': eLpNorm'(-f) q μ = eLpNorm' f q μ.

Русский

В общем случае отрицание не влияет на eLpNorm': eLpNorm'(-f) q μ = eLpNorm'(f) q μ.

LaTeX

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

Lean4

@[simp]
theorem eLpNorm'_neg (f : α → F) (q : ℝ) (μ : Measure α) : eLpNorm' (-f) q μ = eLpNorm' f q μ := by
  simp [eLpNorm'_eq_lintegral_enorm]

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

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

Разделы

Аффилиация

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