cond_add_cond_compl_eq — Mathlib

English

Equality of conditioned measures on S and on S ∩ T under measurability and finiteness assumptions.

Русский

Считается равенство условных мер на S и на S ∩ T при условиях измеримости и конечности.

LaTeX

$$$\\text{MeasurableSet}(S) \\land \\text{MeasurableSet}(T) \\land μ(S) \\neq ∞ \\Rightarrow μ[|S][|T] = μ[|S \\cap T]$$$

Lean4

/-- A version of the law of total probability. -/
theorem cond_add_cond_compl_eq (hms : MeasurableSet s) (μ : Measure Ω) [IsFiniteMeasure μ] :
    μ[t | s] * μ s + μ[t | sᶜ] * μ sᶜ = μ t :=
  by
  rw [cond_mul_eq_inter hms, cond_mul_eq_inter hms.compl, Set.inter_comm _ t, Set.inter_comm _ t]
  exact measure_inter_add_diff t hms

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