eLpNorm_measure_zero — Mathlib

English

For any function f, eLpNorm f p (0) = 0 for any p. The Lp-norm of any function with respect to the zero measure vanishes.

Русский

Для любой функции f норма eLp по нулевой мере равна нулю: eLpNorm f p (0) = 0.

LaTeX

$$$eLpNorm f p (0) = 0$$$

Lean4

@[simp]
theorem eLpNorm_measure_zero {f : α → ε} : eLpNorm f p (0 : Measure α) = 0 :=
  by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simp [h_top]
  rw [← Ne] at h0
  simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', ENNReal.toReal_pos h0 h_top]

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