indicator — Mathlib

English

If f is locally integrable, then the product with an indicator of a measurable set is locally integrable.

Русский

Если f локально интегрируема, то произведение f на индикатор измеримого множества тоже локально интегрируемо.

LaTeX

$$$\\operatorname{LocallyIntegrable}(f) \\Rightarrow \\forall s\\text{ Measurable}, \\operatorname{LocallyIntegrable}(s.indicator(f))$$$

Lean4

theorem indicator {f : X → ε''} (hf : LocallyIntegrable f μ) {s : Set X} (hs : MeasurableSet s) :
    LocallyIntegrable (s.indicator f) μ := by
  intro x
  rcases hf x with ⟨U, hU, h'U⟩
  exact ⟨U, hU, h'U.indicator hs⟩

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