eLpNorm'_norm — Mathlib

English

Same relation as above for indicator sub indicator, expressed with indicator of symmetric difference.

Русский

Та же связь для индикаторов, выраженная через индикатор симметрической разности.

LaTeX

$$$eLpNorm\bigl(\mathbf{1}_s f - \mathbf{1}_t f\bigr)\, p\, μ = eLpNorm\bigl((s\Delta t)\mathbf{1}_f\bigr)\, p\, μ.$$$

Lean4

@[simp]
theorem eLpNorm'_norm {f : α → F} : eLpNorm' (fun a => ‖f a‖) q μ = eLpNorm' f q μ := by
  simp [eLpNorm'_eq_lintegral_enorm]

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