English
Let c be a fixed element and assume its EN-norm is not infinite. Then for any nonzero p with p ≠ ∞, eLpNorm of the constant c is finite if and only if either c = 0 or μ(univ) < ∞.
Русский
Пусть константа c имеет конечную EN-норму; тогда для p ≠ 0, ∞ норма eLp равна конечной тогда и только тогда, когда c = 0 или μ(общее множество) < ∞.
LaTeX
$$$eLpNorm(\\lambda x. c) p μ < \\infty \\iff \\|c\\|_e = 0 \\lor μ(\\mathrm{univ}) < \\infty$$$
Lean4
theorem eLpNorm_const_lt_top_iff_enorm {c : ε''} (hc' : ‖c‖ₑ ≠ ∞) {p : ℝ≥0∞} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
eLpNorm (fun _ : α ↦ c) p μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞ :=
by
have hp : 0 < p.toReal := ENNReal.toReal_pos hp_ne_zero hp_ne_top
by_cases hμ : μ = 0
· simp only [hμ, Measure.coe_zero, Pi.zero_apply, or_true, ENNReal.zero_lt_top, eLpNorm_measure_zero]
by_cases hc : ‖c‖ₑ = 0
· rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_ne_zero hp_ne_top]
simp [hc, ENNReal.zero_rpow_of_pos hp]
rw [eLpNorm_const' c hp_ne_zero hp_ne_top]
obtain hμ_top | hμ_ne_top := eq_or_ne (μ .univ) ∞
· simp [hc, hμ_top, hp]
rw [ENNReal.mul_lt_top_iff]
simpa [hμ, hc, hμ_ne_top, hμ_ne_top.lt_top, hc'.lt_top] using by finiteness
