cond_apply'

Mathlib.Probability.ConditionalProbability

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.cond_apply'

← MathLib Explorer

English

Variant of cond_apply requiring measurability of t.

Русский

Вариант cond_apply, требующий измеримости множества t.

LaTeX

$$$cond\\_apply'(ht : MeasurableSet t) (μ : Measure Ω) : μ[t|s] = (μ s)^{-1} μ(s ∩ t)$$$

Lean4

theorem cond_apply' (ht : MeasurableSet t) (μ : Measure Ω) : μ[t | s] = (μ s)⁻¹ * μ (s ∩ t) := by
  rw [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]

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

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

Разделы

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

Аффилиация

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