eLpNorm_const_lt_top_iff — Mathlib

English

For a nonzero constant c and finite, nontrivial μ, eLpNorm of the constant is finite if and only if c = 0 or μ(univ) < ∞, provided p ≠ 0 and p ≠ ∞.

Русский

Для константы c ≠ 0 и конечной меры μ норма eLp константы конечна тогда и только тогда, когда c = 0 или μ(общее множество) < ∞, при условии p ≠ 0, ∞.

LaTeX

$$$eLpNorm(\\lambda x. c) p μ < \\infty \\iff c = 0 \\lor μ(\\mathrm{univ}) < \\infty$$$

Lean4

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

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