enorm_rpow — Mathlib

English

If f ∈ Lp and p>0, p<∞, then the EN-norm power of f lies in L1, i.e., ∥f∥^p ∈ L1.

Русский

Если f ∈ Lp и 0<p<∞, то степень EN-нормы ∥f∥^p принадлежит L1.

LaTeX

$$$MemLp\ (\|f\|_E^p)\ 1\ μ$$$

Lean4

theorem enorm_rpow {f : α → ε} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    MemLp (fun x : α => ‖f x‖ₑ ^ p.toReal) 1 μ :=
  by
  convert hf.enorm_rpow_div p
  rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

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