cond_isProbabilityMeasure_of_finite

English

Negating the random variable does not change the conditional variance.

Русский

Отрицание переменной не меняет условную дисперсию.

LaTeX

$$$\\mathrm{Var}[-X; μ | m] =^a.e_ μ \\; \\mathrm{Var}[X; μ | m]$$$

Lean4

/-- The conditional probability measure of any measure on any set of finite positive measure
is a probability measure. -/
theorem cond_isProbabilityMeasure_of_finite (hcs : μ s ≠ 0) (hs : μ s ≠ ∞) : IsProbabilityMeasure μ[|s] :=
  ⟨by
    unfold ProbabilityTheory.cond
    simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul]
    exact ENNReal.inv_mul_cancel hcs hs⟩

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