dist_indicatorConstLp_eq_norm — Mathlib

English

A family of indicatorConstLp functions is continuous in the parameter if μ(t_b Δ s) → 0 as b → x; then indicatorConstLp converges to indicatorConstLp(p, hs, hμs, c).

Русский

Семейство indicatorConstLp непрерывно по параметру при сходящемся к нулю мерам симм. разности; индикатор сходится к пределу.

LaTeX

$$$\text{tendsto indicatorConstLp set lemma: }$ (informal) $$\lim_{b\to x} indicatorConstLp(p,ht_b, hμt_b,c) = indicatorConstLp(p, hs, hμs, c).$$$$

Lean4

theorem dist_indicatorConstLp_eq_norm {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ∞} :
    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‖ :=
  by
  -- Squeezed for performance reasons
  simp only [Lp.dist_edist, edist_indicatorConstLp_eq_enorm, enorm, ENNReal.coe_toReal, Lp.coe_nnnorm]

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