English
The conditional CDF ρ a is defined as the Stieltjes transform of the measurable rat function a ↦ (preCDF ρ r a)^{toReal}, i.e., condCDF ρ a := stieltjesOfMeasurableRat (r ↦ (preCDF ρ r a)^{toReal}) measurable_preCDF' a.
Русский
Условная функция распределения ρ a определяется как преобразование Стилтьджеса измеримой функции, задаваемой по a: condCDF ρ a := stieltjesOfMeasurableRat (r ↦ (preCDF ρ r a)^{toReal}) мерная_предпCDF' a.
LaTeX
$$$\\text{condCDF}(ρ,a) := \\; \\mathrm{stieltjesOfMeasurableRat}\\Bigl( (p,r) \\mapsto (\\mathrm{preCDF}(ρ,r,p))^{\\mathrmReal} \\Bigr) (\\text{measurable_preCDF}' , a).$$$
Lean4
/-- Conditional cdf of the measure given the value on `α`, as a Stieltjes function. -/
noncomputable def condCDF (ρ : Measure (α × ℝ)) (a : α) : StieltjesFunction :=
stieltjesOfMeasurableRat (fun a r ↦ (preCDF ρ r a).toReal) measurable_preCDF' a
