eLpNorm_neg — Mathlib

English

The ordinary eLpNorm is invariant under negation: eLpNorm(-f) p μ = eLpNorm(f) p μ.

Русский

Обычная eLpNorm инвариантна к отрицанию: eLpNorm(-f) p μ = eLpNorm(f) p μ.

LaTeX

$$$eLpNorm(-f)\\, p \\,\\mu = eLpNorm(f)\\, p \\,\\mu$$$

Lean4

@[simp]
theorem eLpNorm_neg (f : α → F) (p : ℝ≥0∞) (μ : Measure α) : eLpNorm (-f) p μ = eLpNorm f p μ :=
  by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simp [h_top, eLpNormEssSup_eq_essSup_enorm]
  simp [eLpNorm_eq_eLpNorm' h0 h_top]

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