cond_eq_inv_mul_cond_mul — Mathlib

English

A version of the law of total probability: μ[T|S] μ[S] + μ[T|Sᶜ] μ[Sᶜ] = μ[T].

Русский

Версия закона полной вероятности: μ[T|S] μ[S] + μ[T|Sᶜ] μ[Sᶜ] = μ[T].

LaTeX

$$$\\mu[T|S] \\cdot μ(S) + μ[T|S^c] \\cdot μ(S^c) = μ(T)$$$

Lean4

/-- **Bayes' Theorem** -/
theorem cond_eq_inv_mul_cond_mul (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : Measure Ω) [IsFiniteMeasure μ] :
    μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t := by rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]

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