lintegral_indicator — Mathlib

English

If s is measurable, then the lintegral of the indicator of f over the whole space equals the lintegral of f over s with respect to μ.restrict s.

Русский

Пусть s измеримо. Тогда линеграл индикатора f по всему пространству равен линегралу f на s по мере μ.restrict s.

LaTeX

$$$$ \\int^- a: \\alpha, s.indicator f(a) \\, d\\mu = \\int^- a \\in s, f(a) \\, d\\mu. $$$$

Lean4

@[simp]
theorem lintegral_indicator {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    ∫⁻ a, s.indicator f a ∂μ = ∫⁻ a in s, f a ∂μ :=
  by
  apply le_antisymm (lintegral_indicator_le f s)
  simp only [lintegral, ← restrict_lintegral_eq_lintegral_restrict _ hs, iSup_subtype']
  refine iSup_mono' (Subtype.forall.2 fun φ hφ => ?_)
  refine ⟨⟨φ.restrict s, fun x => ?_⟩, le_rfl⟩
  simp [hφ x, hs, indicator_le_indicator]

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