eLpNorm'_eq — Mathlib

English

Explicit formula for the eLp norm of a simple function: sum over its range of ∥y∥^p times the measure of its preimage of {y}, then raised to the 1/p.

Русский

Явная формула нормы eLp простой функции: сумма по значениям функции ∥y∥^p μ(f^{-1}({y})), возведение в степень 1/p.

LaTeX

$$$\\mathrm{eLpNorm}'(f,p,\\mu) = \\Big(\\sum_{y\\in f.range} \\|y\\|_{E}^{\,p}\\, \\mu(f^{-1} \\{y\\})\\Big)^{1/p}$$$

Lean4

protected theorem eLpNorm'_eq {p : ℝ} (f : α →ₛ F) (μ : Measure α) :
    eLpNorm' f p μ = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (f ⁻¹' { y })) ^ (1 / p) :=
  by
  have h_map : (‖f ·‖ₑ ^ p) = f.map (‖·‖ₑ ^ p) := by simp; rfl
  rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]

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