measurable_measure_condCDF — Mathlib

English

Let ρ be a probability measure on α × ℝ. Then the map a ↦ (condCDF ρ a).measure is measurable.

Русский

Пусть ρ — распределение вероятности на α × ℝ. Тогда отображение a ↦ (condCDF ρ a).measure является измеримым.

LaTeX

$$$\mathsf{Measurable}\big( a \mapsto (\mathrm{condCDF}\ \rho\ a).\mathrm{measure} \big)$$$

Lean4

/-- The function `a ↦ (condCDF ρ a).measure` is measurable. -/
theorem measurable_measure_condCDF (ρ : Measure (α × ℝ)) : Measurable fun a => (condCDF ρ a).measure :=
  .measure_of_isPiSystem_of_isProbabilityMeasure (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic <|
    by
    simp_rw [forall_mem_range, measure_condCDF_Iic]
    exact fun u ↦ (measurable_condCDF ρ u).ennreal_ofReal

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