English
Negation of the function argument keeps the eLpNorm' unchanged: eLpNorm'(−f) q μ = eLpNorm'(f) q μ.
Русский
Отрицание аргумента функции сохраняет eLpNorm': eLpNorm'(−f) q μ = eLpNorm'(f) q μ.
LaTeX
$$$eLpNorm'(-f)\\, q \\,\\mu = eLpNorm'(f)\\, q \\,\\mu$$$
Lean4
theorem eLpNorm'_const (c : ε) (hq_pos : 0 < q) : eLpNorm' (fun _ : α => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q) :=
by
rw [eLpNorm'_eq_lintegral_enorm, lintegral_const, ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)]
congr
rw [← ENNReal.rpow_mul]
suffices hq_cancel : q * (1 / q) = 1 by rw [hq_cancel, ENNReal.rpow_one]
rw [one_div, mul_inv_cancel₀ (ne_of_lt hq_pos).symm]
-- Generalising this to ESeminormedAddMonoid requires a case analysis whether ‖c‖ₑ = ⊤,
-- and will happen in a future PR.
