measure_condCDF_univ — Mathlib

English

For any a, condCDF ρ a equals stieltjesOfMeasurableRat_unit_prod applied to the pair ((), a).

Русский

Для каждого a condCDF ρ a равен применению к паре ((), a) функции stieltjesOfMeasurableRat_unit_prod.

LaTeX

$$$condCDF(ρ,a) = stieltjesOfMeasurableRat (fun (p : Unit × α) r ↦ (preCDF ρ r p.2).toReal) ( Measurable...) ((),a).$$$

Lean4

theorem measure_condCDF_univ (ρ : Measure (α × ℝ)) (a : α) : (condCDF ρ a).measure univ = 1 :=
  by
  rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]
  exact StieltjesFunction.measure_univ _ (tendsto_condCDF_atBot ρ a) (tendsto_condCDF_atTop ρ a)

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