setIntegral_indicator — Mathlib

English

Let t be a measurable set. For any function f, the integral of f against the indicator of t over a set s equals the integral of f over the intersection s ∩ t.

Русский

Пусть t — измеримое множество. Для любой функции f интеграл f по мере μ на множествах s и t совпадает с интегралом по пересечению s ∩ t: ∫_s t(x) f(x) dμ = ∫_{s∩t} f(x) dμ.

LaTeX

$$$ \int_{x \in s} \mathbf{1}_{t}(x) f(x) \, d\mu = \int_{x \in s \cap t} f(x) \, d\mu $$$

Lean4

theorem setIntegral_indicator (ht : MeasurableSet t) : ∫ x in s, t.indicator f x ∂μ = ∫ x in s ∩ t, f x ∂μ := by
  rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]

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