English
For a fixed constant c, eLpNorm'(f) of a constant function equals ∥c∥ times the real power of μ(univ) with exponent 1/q, i.e., eLpNorm'(const c) q μ = ∥c∥ₑ μ(univ)^(1/q).
Русский
Для константы c норма eLpNorm' константы равна ∥c∥ умножить на μ(всё множество)^(1/q).
LaTeX
$$eLpNorm' (fun _ => c) q μ = ∥c∥ₑ * μ(1)^(1/q)$$
Lean4
theorem eLpNorm'_const' [IsFiniteMeasure μ] (c : F) (hc_ne_zero : c ≠ 0) (hq_ne_zero : q ≠ 0) :
eLpNorm' (fun _ : α => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q) :=
by
rw [eLpNorm'_eq_lintegral_enorm, lintegral_const, ENNReal.mul_rpow_of_ne_top _ (measure_ne_top μ Set.univ)]
· congr
rw [← ENNReal.rpow_mul]
suffices hp_cancel : q * (1 / q) = 1 by rw [hp_cancel, ENNReal.rpow_one]
rw [one_div, mul_inv_cancel₀ hq_ne_zero]
· have : ‖c‖ₑ ≠ 0 := by simp [hc_ne_zero]
finiteness
