integrable_condCDF — Mathlib

English

For fixed x, the function a ↦ (condCDF ρ a x)^{toFun} is integrable with respect to ρ.fst.

Русский

Для фиксированного x функция a ↦ (condCDF ρ a x)^{toFun} интегрируема по ρ.fst.

LaTeX

$$$\\text{Integrable}_{ρ_fst}(a \\mapsto (condCDF(ρ,a,x))^{\\mathrm{toFun}}).$$$

Lean4

theorem integrable_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x : ℝ) :
    Integrable (fun a ↦ condCDF ρ a x) ρ.fst :=
  (isCondKernelCDF_condCDF ρ).integrable () x

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