lintegral_rpow_enorm_eq_rpow_eLpNorm'

English

For q>0, the lintegral of ‖f‖^q equals (eLpNorm'(f,q,μ))^q.

Русский

Для q>0 линтеграл от ‖f‖^q равен (eLpNorm'(f,q,μ))^q.

LaTeX

$$$\\int^{\\! -} a\\; \\|f(a)\\|_{\\varepsilon}^{\\,q} \\partial\\mu(a) = \\big(\\mathrm{eLpNorm}'(f,q,\\mu)\\big)^{q}$$$

Lean4

theorem lintegral_rpow_enorm_eq_rpow_eLpNorm' {f : α → ε} (hq0_lt : 0 < q) : ∫⁻ a, ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q :=
  by
  rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div, inv_mul_cancel₀, ENNReal.rpow_one]
  exact hq0_lt.ne'

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