essSup_indicator_eq_essSup_restrict

English

If μ is absolutely continuous with respect to ν, then essInf f ν ≤ essInf f μ.

Русский

Если μ абсолюьтно непрерывна по ν, то essInf f ν ≤ essInf f μ.

LaTeX

$$$$ \\operatorname{essInf} f \\nu \\le \\operatorname{essInf} f \\mu \\quad \\text{if } \\mu \\ll \\nu $$$$

Lean4

theorem essSup_indicator_eq_essSup_restrict {s : Set α} {f : α → ℝ≥0∞} (hs : MeasurableSet s) :
    essSup (s.indicator f) μ = essSup f (μ.restrict s) := by
  classical
  simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]
  exact limsup_const_bot.trans_le (zero_le _)

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