setLIntegral_condCDF — Mathlib

English

For a measurable s ⊆ α, the left-hand integral of ENNReal.ofReal(condCDF ρ a x) over s w.r.t. ρ.fst equals ρ(s × (-∞, x]).

Русский

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

LaTeX

$$$\\int_{a \\in s} ENNReal.ofReal(condCDF(ρ,a,x)) \\, dρ.fst(a) = ρ(s \\times\\! Iic(x)).$$$

Lean4

theorem setLIntegral_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℝ) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ a in s, ENNReal.ofReal (condCDF ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x) :=
  (isCondKernelCDF_condCDF ρ).setLIntegral () hs x

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