cond_absolutelyContinuous

Mathlib.Probability.ConditionalProbability

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.cond_absolutelyContinuous

English

The conditional measure μ[|s] is absolutely continuous with respect to μ.

Русский

Условная мера μ[|s] абсолютно непрерывна по отношению к μ.

LaTeX

$$$\\mu[|s] \\ll \\mu$$$

Lean4

theorem cond_absolutelyContinuous : μ[|s] ≪ μ :=
  smul_absolutelyContinuous.trans restrict_le_self.absolutelyContinuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru