English
Let p be a nonzero, finite exponent and c a fixed element with finite ENorm. Then the constant function x ↦ c is in the Lp space Lp(μ) if and only if either c = 0 or the whole space has finite μ-measure (i.e., μ(α) < ∞).
Русский
Пусть p не равен 0 и не равен ∞, и c имеет конечную ENorm. Тогда константная функция x ↦ c принадлежит пространству Lp(μ) тогда и только тогда, когда либо c = 0, либо вся пространство имеет конечную меру: μ(α) < ∞.
LaTeX
$$$\\operatorname{MemLp}( \\lambda x: c )\\; p\\; μ \\;\\Longleftrightarrow\\; \\|c\\|_ε = 0 \\;\\lor\\; μ(\\mathrm{univ}) < ∞,$ при $p \\neq 0$ и $p \\neq ∞$ и $\\|c\\|_ε \\neq ∞$.$$
Lean4
theorem memLp_const_iff_enorm {p : ℝ≥0∞} {c : ε''} (hc : ‖c‖ₑ ≠ ⊤) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
MemLp (fun _ : α ↦ c) p μ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞ := by
simp_all [MemLp, aestronglyMeasurable_const, eLpNorm_const_lt_top_iff_enorm hc hp_ne_zero hp_ne_top]
