isCondKernelCDF_condKernelCDF — Mathlib

English

The auxiliary lemma shows that the conditional kernel CDF built from κ has the same structure when we truncate via Iic, connecting to the base κ.

Русский

Лемма-замещатель показывает, что условное ядро CDF, построенное из κ, сохраняет структуру при ограничении через Iic и связано с базовым κ.

LaTeX

$$IsCondKernelCDF( (p,q) => κ.density κ.fst p.1 p.2 (Iic q.cast) ) κ (κ.fst)$$

Lean4

theorem isCondKernelCDF_condKernelCDF (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    IsCondKernelCDF (condKernelCDF κ) κ (fst κ) :=
  isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_density_Iic κ)

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