memLp_const_iff — Mathlib

English

For a constant function with a fixed value c in a normed real target, the same criterion as above holds: MemLp(λx. c) p μ is equivalent to c = 0 or μ(α) < ∞, under the same constraints on p.

Русский

Для константной функции значения c в нормированном пространстве над реальными числами действует то же условие: MemLp(λx. c) p μ эквивалентно c = 0 или μ(α) < ∞, при тех же ограничениях на p.

LaTeX

$$$\\operatorname{MemLp}( \\lambda x: c)\\; p\\; μ \\;\\Longleftrightarrow\\; c = 0 \\;\\lor\\; μ(\\mathrm{univ}) < ∞,$ при $p \\neq 0$ и $p \\neq ∞$.$$

Lean4

theorem memLp_const_iff {p : ℝ≥0∞} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    MemLp (fun _ : α => c) p μ ↔ c = 0 ∨ μ Set.univ < ∞ := by
  rw [memLp_const_iff_enorm enorm_ne_top hp_ne_zero hp_ne_top]; simp

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