condCDF_eq_stieltjesOfMeasurableRat_unit_prod

English

For a finite measure ρ, the conditional CDF satisfies condCDF ρ a = stieltjesOfMeasurableRat (fun (p : Unit × α) r ↦ (preCDF ρ r p.2).toReal) (measurable_preCDF'.comp measurable_snd) ((), a).

Русский

Для конечной меры ρ условная функция CDF удовлетворяет равенству condCDF ρ a = stieltjesOfMeasurableRat (…) ((), a).

LaTeX

$$$\\mathrm{condCDF}(ρ,a) = \\mathrm{stieltjesOfMeasurableRat}\\bigl( (p,r)\\mapsto (\\mathrm{preCDF}(ρ,r,p.2))^{\\mathrm{toReal}} \\bigr) (\\mathrm{measurable_preCDF'}.\\mathrmcomp \\mathrm snd) ((),a).$$$

Lean4

theorem condCDF_eq_stieltjesOfMeasurableRat_unit_prod (ρ : Measure (α × ℝ)) (a : α) :
    condCDF ρ a =
      stieltjesOfMeasurableRat (fun (p : Unit × α) r ↦ (preCDF ρ r p.2).toReal) (measurable_preCDF'.comp measurable_snd)
        ((), a) :=
  by
  ext x
  rw [condCDF, ← stieltjesOfMeasurableRat_unit_prod]

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