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]