eLpNorm_nnreal_eq_lintegral — Mathlib

English

For p in NNReal, eLpNorm with p equals the corresponding lintegral formulation with p viewed as a real exponent.

Русский

Для p∈NNReal имеем: eLpNorm f p μ = (∫⁻ ‖f‖^{p} dμ)^{1/p} (с п, приведенным к действительному).

LaTeX

$$$eLpNorm\\,f\\,p\\,\\mu = \\left(\\int^{-} a\\; \\|f(a)\\|_{\\varepsilon}^{\\,p.toReal} \\partial\\mu(a)\\right)^{1/p.toReal}$$

Lean4

theorem eLpNorm_nnreal_eq_lintegral {f : α → ε} {p : ℝ≥0} (hp : p ≠ 0) :
    eLpNorm f p μ = (∫⁻ x, ‖f x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) :=
  eLpNorm_nnreal_eq_eLpNorm' hp

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