norm_rpow — Mathlib

English

If f ∈ Lp with p>0 and finite, then the p-th power of the norm is integrable with unit exponent; i.e., ∥f∥^p ∈ L1.

Русский

Если f ∈ Lp при p>0 и p<∞, то ∥f∥^p интегрируемо в L1.

LaTeX

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

Lean4

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

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