instIsProbabilityMeasureCondCDF — Mathlib

English

There is a canonical IsProbabilityMeasure structure associated to condCDF ρ a for each a, i.e., condCDF ρ a is a probability distribution on ℝ when viewed as a measure.

Русский

Для каждого a существует каноническая структура IsProbabilityMeasure, связанная с condCDF ρ a, то есть condCDF ρ a является распределением по ℝ.

LaTeX

$$$IsProbabilityMeasure\\big( condCDF(ρ,a).\\mathrm{measure} \\big).$$$

Lean4

instance instIsProbabilityMeasureCondCDF (ρ : Measure (α × ℝ)) (a : α) : IsProbabilityMeasure (condCDF ρ a).measure :=
  ⟨measure_condCDF_univ ρ a⟩

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