setIntegral_condCDF — Mathlib

English

For measurable s ⊆ α, the real-valued set integral ∫ a∈s condCDF ρ a x^{toFun} dρ.fst(a) equals ρ.real(s × (-∞, x]).

Русский

Для измеримого s ⊆ α интеграл по s вещественного condCDF ρ a x по ρ.fst равен ρ.real(s × (-∞, x]).

LaTeX

$$$\\int_{a \\in s} (condCDF(ρ,a,x))^{\\mathrm{toFun}} dρ.fst(a) = ρ.real(s \\times\\! Iic(x)).$$$

Lean4

theorem setIntegral_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℝ) {s : Set α} (hs : MeasurableSet s) :
    ∫ a in s, condCDF ρ a x ∂ρ.fst = ρ.real (s ×ˢ Iic x) :=
  (isCondKernelCDF_condCDF ρ).setIntegral () hs x

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