measurable_preCDF

Mathlib.Probability.Kernel.Disintegration.CondCDF

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

English

For any rational r, the function a ↦ preCDF ρ r a is measurable.

Русский

Для любого рационального r функция a ↦ preCDF ρ r a измеряема.

LaTeX

$$$\text{Measurable}(preCDF\,\rho\, r)$$$

Lean4

theorem measurable_preCDF {ρ : Measure (α × ℝ)} {r : ℚ} : Measurable (preCDF ρ r) :=
  Measure.measurable_rnDeriv _ _

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

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

Разделы

Аффилиация

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