integral_condExp_indicator — Mathlib

English

Using condExp as a conditional probability, the integral of a specific expression reduces to the real measure of a set.

Русский

Используя condExp как условную вероятность, интеграл по выражению сводится к мере множества.

LaTeX

$$$$\\int x, (\\mu[(A_column) | m]\\, x) \\, d\\mu(x) = \\mu.real(A).$$$$

Lean4

/-- **Law of total probability** using `condExp` as conditional probability. -/
theorem integral_condExp_indicator [mβ : MeasurableSpace β] {Y : α → β} (hY : Measurable Y)
    [SigmaFinite (μ.trim hY.comap_le)] {A : Set α} (hA : MeasurableSet A) :
    ∫ x, (μ[(A.indicator fun _ ↦ (1 : ℝ))|mβ.comap Y]) x ∂μ = μ.real A := by
  rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]

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