stronglyMeasurable_condCDF — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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