eLpNorm'_measure_zero_of_pos — Mathlib

English

If the measure is the zero measure, then the eLpNorm' of any function is zero provided the exponent is nonzero and positive (with the usual conventions when q = 0 or q = ∞ handled separately).

Русский

Если мера равна нулевой, то eLpNorm' любой функции равен нулю при неравенстве q ≠ 0 и соответствующих условиях на q = 0 или q = ∞.

LaTeX

$$$eLpNorm'(f, q, 0) = 0 \\quad\\text{для } 0 < q,$$

Lean4

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

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