measurable_condCDF — Mathlib

English

For fixed ρ and x, the map a ↦ condCDF ρ a x is a measurable function of a.

Русский

Для фиксированного ρ и фиксированного x отображение a ↦ condCDF ρ a x измеримо по a.

LaTeX

$$$a \\mapsto condCDF(ρ,a) \\\\text{ is measurable at } x.$$$

Lean4

/-- The conditional cdf is a measurable function of `a : α` for all `x : ℝ`. -/
theorem measurable_condCDF (ρ : Measure (α × ℝ)) (x : ℝ) : Measurable fun a ↦ condCDF ρ a x :=
  measurable_stieltjesOfMeasurableRat _ _

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