condKernelCDF — Mathlib

English

The conditional kernel CDF of κ is itself a conditional kernel CDF with respect to κ: IsCondKernelCDF (condKernelCDF κ) κ (fst κ).

Русский

Условная функция распределения ядра κ сама имеет свойство IsCondKernelCDF относительно κ: IsCondKernelCDF(condKernelCDF κ) κ (fst κ).

LaTeX

$$IsCondKernelCDF( condKernelCDF κ ) κ (fst κ)$$

Lean4

/-- The conditional kernel CDF of a kernel `κ : Kernel α (γ × ℝ)`, where `γ` is countably generated.
-/
noncomputable def condKernelCDF (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : α × γ → StieltjesFunction :=
  stieltjesOfMeasurableRat (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q))
    (isRatCondKernelCDF_density_Iic κ).measurable

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