condKernelUnitReal — Mathlib

English

For κ : Kernel Unit (Prod α Real) finite, κ.condKernelUnitReal equals the IsCondKernelCDF-to-Kernel construction based on κ.

Русский

Для κ: Kernel Unit (Prod α Real) конечного типа, κ.condKernelUnitReal равняется конструктору IsCondKernelCDF к κ.

LaTeX

$$$\kappa.condKernelUnitReal = IsCondKernelCDF.toKernel(\text{something involving } \kappa)$$$

Lean4

/-- Auxiliary definition for `MeasureTheory.Measure.condKernel` and
`ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel Unit (α × ℝ)`. -/
noncomputable def condKernelUnitReal (κ : Kernel Unit (α × ℝ)) [IsFiniteKernel κ] : Kernel (Unit × α) ℝ :=
  (isCondKernelCDF_condCDF (κ ())).toKernel

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