setLIntegral_inter_eq_indicator_mul_setLIntegral

English

For a proper kernel π and measurable A,B, the l-integral over A ∩ B with function f equals B.indicator(1) at x0 times the l-integral over A of f, reflecting a cross-section property of π.

Русский

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

LaTeX

$$$$ \int_{A\cap B} f(x) dπ_x = \mathbf{1}_B(x_0) \int_A f(x) dπ_x. $$$$

Lean4

theorem setLIntegral_inter_eq_indicator_mul_setLIntegral (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable[𝓧] f)
    (hA : MeasurableSet[𝓧] A) (hB : MeasurableSet[𝓑] B) (x₀ : X) :
    ∫⁻ x in A ∩ B, f x ∂(π x₀) = B.indicator 1 x₀ * ∫⁻ x in A, f x ∂(π x₀) := by
  rw [← lintegral_indicator hA, ← hπ.setLIntegral_eq_indicator_mul_lintegral h𝓑𝓧 _ hB, setLIntegral_indicator] <;>
    measurability

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