eLpNorm_eq_lintegral_rpow_enorm — Mathlib

English

For p>0, the Lp norm equals the q-power lintegral representation with p.toReal.

Русский

Для p>0 имеем: eLpNorm(f,p,μ) = (∫⁻ ‖f‖^{p.toReal} dμ)^{1/p.toReal}.

LaTeX

$$$eLpNorm\\,f\\,p\\,\\mu = \\left(\\int^{-}\\|f(x)\\|_{\\varepsilon}^{\\,p^{\\mathrm{toReal}}} \\mathrm{d}\\mu(x)\\right)^{1/p^{\\mathrm{toReal}}}$$

Lean4

theorem eLpNorm_eq_lintegral_rpow_enorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε} :
    eLpNorm f p μ = (∫⁻ x, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) := by
  rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top, eLpNorm'_eq_lintegral_enorm]

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