eLpNorm'_eq_lintegral_enorm — Mathlib

English

The quantity eLpNorm' is equal to the lintegral representation (the defining form), i.e., eLpNorm'(f,q,μ) = (∫⁻ ‖f‖^q dμ)^{1/q}.

Русский

Количество eLpNorm' равно линтегралу: eLpNorm'(f,q,μ) = (∫⁻ ‖f‖^q dμ)^{1/q}.

LaTeX

$$$\\mathrm{eLpNorm}'(f,q,\\mu) = \\left(\\int^{\\!-}\\|f(a)\\|_{\\varepsilon}^{\\,q} \\\\mathrm{d}\\mu(a)\\right)^{1/q}$$$

Lean4

theorem eLpNorm'_eq_lintegral_enorm {_ : MeasurableSpace α} (f : α → ε) (q : ℝ) (μ : Measure α) :
    eLpNorm' f q μ = (∫⁻ a, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) :=
  rfl

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