eLpNorm_indicator_sub_indicator — Mathlib

English

The Lp-norm of the difference of two indicator functions is the same as the Lp-norm of the indicator of their symmetric difference.

Русский

Норма Lp разности двух индикаторных функций равна норме Lp индикатора симметрической разности.

LaTeX

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

Lean4

theorem eLpNorm_indicator_sub_indicator (s t : Set α) (f : α → E) :
    eLpNorm (s.indicator f - t.indicator f) p μ = eLpNorm ((s ∆ t).indicator f) p μ :=
  eLpNorm_congr_norm_ae <| ae_of_all _ fun x ↦ by simp [Set.apply_indicator_symmDiff norm_neg]

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