isCondKernelCDF_condCDF — Mathlib

English

The family a ↦ condCDF ρ a forms an IsCondKernelCDF with the kernel const Unit ρ and the kernel const Unit ρ.fst, i.e., the conditional CDF defines a conditional kernel.

Русский

Семейство a ↦ condCDF ρ a образует IsCondKernelCDF с ядрами const Unit ρ и const Unit ρ.fst; условное CDF задаёт условное ядро.\n

LaTeX

$$$IsCondKernelCDF\\left( a \\mapsto condCDF(ρ,a),\\; Kernel.const\\, Unit\\, ρ,\\; Kernel.const\\, Unit\\, ρ.fst \\right).$$$

Lean4

theorem isCondKernelCDF_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    IsCondKernelCDF (fun p : Unit × α ↦ condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst) :=
  by
  simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]
  exact isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_preCDF ρ)

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