eLpNorm_norm — Mathlib

English

For q>0, eLpNorm of |f|^q equals the q-th power of eLpNorm of f scaled by p and q: eLpNorm'(|f|^q) using p and q relation.

Русский

При q>0, eLpNorm(|f|^q) выражается через eLpNorm(f) с отношением p и q.

LaTeX

$$$eLpNorm\,\bigl(\|f\|^q\bigr)\; p\; μ = eLpNorm\,f\; (p\cdot q)\; μ^q \quad (q>0).$$$

Lean4

@[simp]
theorem eLpNorm_norm (f : α → F) : eLpNorm (fun x => ‖f x‖) p μ = eLpNorm f p μ :=
  eLpNorm_congr_norm_ae <| Eventually.of_forall fun _ => norm_norm _

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