indicator_ae_eq_of_restrict_compl_ae_eq_zero

English

If s is measurable and f =ᵐ[μ|_s^c] 0, then s.indicator f =ᵐ[μ] f.

Русский

Если s измеримо и f равно нулю почти повсеместно на s^c, то индикатор sf равен f почти повсеместно.

LaTeX

$$$ \\text{indicator } s\\, f =_{\\mathrm{ae}}^{\\mu} f $ under the hypothesis.$$

Lean4

theorem indicator_ae_eq_of_restrict_compl_ae_eq_zero (hs : MeasurableSet s) (hf : f =ᵐ[μ.restrict sᶜ] 0) :
    s.indicator f =ᵐ[μ] f := by
  rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at hf
  filter_upwards [hf] with x hx
  by_cases hxs : x ∈ s
  · simp only [hxs, Set.indicator_of_mem]
  · simp only [hx hxs, Pi.zero_apply, Set.indicator_apply_eq_zero, imp_true_iff]

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