lintegral_condCDF — Mathlib

English

For any x, the lintegral over α of ENNReal.ofReal(condCDF ρ a x) with respect to ρ.fst equals ρ(univ × (-∞, x]).

Русский

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

LaTeX

$$$\\operatorname{lintegral}_{a} ENNReal.ofReal(condCDF(ρ,a,x))\\, dρ.fst(a) = ρ(\\\\mathrm{univ} \\times Iic(x)).$$$

Lean4

theorem lintegral_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℝ) :
    ∫⁻ a, ENNReal.ofReal (condCDF ρ a x) ∂ρ.fst = ρ (univ ×ˢ Iic x) :=
  (isCondKernelCDF_condCDF ρ).lintegral () x

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