absolutelyContinuous_cond_univ — Mathlib

English

The conditional probability μ|univ is absolutely continuous with respect to μ.

Русский

Условная вероятность по всему пространству равна абсолютоной непрерывности относительно μ.

LaTeX

$$$μ \\ll μ[|univ]$$$

Lean4

theorem absolutelyContinuous_cond_univ [IsFiniteMeasure μ] : μ ≪ μ[|univ] :=
  by
  rw [cond, restrict_univ]
  refine absolutelyContinuous_smul ?_
  simp [measure_ne_top]

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