English
For every a in α, the map b ↦ Kernel.condKernel κ (a, b) is almost everywhere equal (with respect to Kernel.fst κ a) to the conditional kernel of the measure κ a.
Русский
Пусть κ : Kernel α (β × Ω) является конечным ядром; для каждого a ∈ α функция b ↦ Kernel.condKernel κ (a, b) почти surely равна условному ядру меры κ a относительно меры Kernel.fst κ a.
LaTeX
$$$( \\lambda b \\mapsto \\mathrm{condKernel}(\\kappa)(a,b) ) =_\\mathrm{ae}^{\\mathrm{fst}(\\kappa)a} (\\kappa a).\\mathrm{condKernel}$$$
Lean4
/-- For `fst κ a`-almost all `b`, the conditional kernel `Kernel.condKernel κ` applied to `(a, b)`
is equal to the conditional kernel of the measure `κ a` applied to `b`. -/
theorem condKernel_apply_eq_condKernel [CountableOrCountablyGenerated α β] (κ : Kernel α (β × Ω)) [IsFiniteKernel κ]
(a : α) : (fun b ↦ Kernel.condKernel κ (a, b)) =ᵐ[Kernel.fst κ a] (κ a).condKernel :=
Kernel.apply_eq_measure_condKernel_of_compProd_eq (κ.disintegrate _) a
