condKernelReal — Mathlib

English

For κ : Kernel α (Prod γ Real) finite, the density with Iic in the Real coordinate defines an IsRatCondKernelCDF with respect to κ.

Русский

Для κ: Kernel α (Prod γ Real) конечного типа плотность по Iic в координате Real образует IsRatCondKernelCDF относительно κ.

LaTeX

$$IsRatCondKernelCDF (\lambda p q. κ.density κ.fst p.fst p.snd (Iic q.cast)) κ (κ.fst)$$

Lean4

/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel α (γ × ℝ)` where `γ` is countably generated. -/
noncomputable def condKernelReal (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] : Kernel (α × γ) ℝ :=
  (isCondKernelCDF_condKernelCDF κ).toKernel

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