zero — Mathlib

English

Let μ be a measure on α and p be a nonnegative exponent. The zero function is p-integrable with respect to μ; equivalently, the constant function f ≡ 0 belongs to the Lp(μ) space for every p, and its Lp-norm is 0.

Русский

Пусть μ — мера на α и p — неотрицательный показатель. Нулевая функция является p-интегрируемой по отношению к μ; то есть постоянная функция f ≡ 0 принадлежит пространству Lp(μ) для любого p, и её Lp-норма равна 0.

LaTeX

$$$0 \in L^p(\\mu)\\quad\\text{and}\\quad \\|0\\|_{L^p(\\mu)} = 0$$$

Lean4

@[simp]
theorem zero : MemLp (0 : α → ε) p μ :=
  ⟨aestronglyMeasurable_zero, by rw [eLpNorm_zero]; exact ENNReal.coe_lt_top⟩

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