eLpNorm_norm_rpow — Mathlib

English

If hg MemLp g p μ, hf AEStronglyMeasurable f μ, and hfg ≤ g almost everywhere, then MemLp f p μ.

Русский

Если hg MemLp g p μ и f измеримо, а |f|≤g a.e., тогда MemLp f p μ.

LaTeX

$$$MemLp g p μ \rightarrow AEStronglyMeasurable f μ \rightarrow (|f| ≤ g) \text{ a.e.} ⇒ MemLp f p μ.$$$

Lean4

theorem eLpNorm_norm_rpow (f : α → F) (hq_pos : 0 < q) :
    eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q :=
  by
  rw [← eLpNorm_enorm_rpow f hq_pos]
  symm
  convert eLpNorm_ofReal (fun x ↦ ‖f x‖ ^ q) (by filter_upwards with x using by positivity)
  rw [Function.comp_apply, ← ofReal_norm_eq_enorm]
  exact ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)

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