setLIntegral_eq_indicator_mul_lintegral

English

For a proper kernel π and B measurable, the lintegral over B of an indicator times density equals the product of the indicator and the lintegral over the whole domain.

Русский

Для правильного ядра π и измеримого B справедливо равенство линегрального интеграла, когда умножаем на индикатор плотности и интеграл по всему домену.

LaTeX

$$$$ \int_B f(x) dπ_x = \mathbf{1}_B(x_0) \int f(x) dπ_x. $$$$

Lean4

theorem setLIntegral_eq_indicator_mul_lintegral (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable[𝓧] f)
    (hB : MeasurableSet[𝓑] B) (x₀ : X) : ∫⁻ x in B, f x ∂(π x₀) = B.indicator 1 x₀ * ∫⁻ x, f x ∂(π x₀) := by
  simp [← hπ.lintegral_indicator_mul h𝓑𝓧 hf hB, ← indicator_mul_left, lintegral_indicator (h𝓑𝓧 _ hB)]

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