integral_condCDF — Mathlib

English

For any ρ finite measure, the integral over a of condCDF ρ a real part x equals the real measure of univ × (-∞, x].

Русский

Для любой конечной меры ρ интеграл по a от condCDF ρ a real x равен вещественной мере всего множества × (-∞, x].

LaTeX

$$$\\int_{a} condCDF(ρ,a)^{toFun}(x)\\, dρ.fst(a) = ρ.real(\\\\mathrm{univ} × Iic(x)).$$$

Lean4

theorem integral_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℝ) :
    ∫ a, condCDF ρ a x ∂ρ.fst = ρ.real (univ ×ˢ Iic x) :=
  (isCondKernelCDF_condCDF ρ).integral () x

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