cond_toMeasurable_eq

Mathlib.Probability.ConditionalProbability

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

← MathLib Explorer

English

The conditional measure μ[t|s] equals (μ s)^{-1} μ(s ∩ t) for measurable s.

Русский

Условная мера μ[t|s] равна (μ(s))^{-1} μ(s ∩ t) при измеримом s.

LaTeX

$$$μ[t|s] = (μ s)^{-1} \\cdot μ(s \\cap t)$$$

Lean4

theorem cond_toMeasurable_eq : μ[|(toMeasurable μ s)] = μ[|s] :=
  by
  unfold cond
  by_cases hnt : μ s = ∞
  · simp [hnt]
  · simp [Measure.restrict_toMeasurable hnt]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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