edist_indicatorConstLp_eq_enorm — Mathlib

English

The distance between indicatorConstLp(p, hs, hμs, c) and indicatorConstLp(p, ht, hμt, c) equals the Lp norm of the indicator on the symmetric difference.

Русский

Расстояние между индикаторами равняется норме Lp индикатора на симм разности.

LaTeX

$$$dist(indicatorConstLp(p, hs, hμs, c), indicatorConstLp(p, ht, hμt, c)) = \|indicatorConstLp(p, hs.symmDiff(ht), measure_symmDiff_ne_top(hμs, hμt), c)\|.$$$

Lean4

theorem edist_indicatorConstLp_eq_enorm {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ∞} :
    edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) =
      ‖indicatorConstLp p (hs.symmDiff ht) (measure_symmDiff_ne_top hμs hμt) c‖ₑ :=
  by
  unfold indicatorConstLp
  rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]

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