lintegral_indicator₀ — Mathlib

English

If s is NullMeasurableSet for μ.restrict t, then the lintegral of s.indicator f over t equals the lintegral over s∩t of f.

Русский

Если s является NullMeasurableSet для μ.restrict t, то интеграл линеграла s.indicator f на t равен интегралу над s∩t.

LaTeX

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

Lean4

theorem lintegral_indicator₀ {s : Set α} (hs : NullMeasurableSet s μ) (f : α → ℝ≥0∞) :
    ∫⁻ a, s.indicator f a ∂μ = ∫⁻ a in s, f a ∂μ := by
  rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    lintegral_indicator (measurableSet_toMeasurable _ _), Measure.restrict_congr_set hs.toMeasurable_ae_eq]

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