English
If ρ is a finite measure on β × Ω, then the conditional kernel of the constant kernel Kernel.const α ρ coincides almost everywhere with ρ.condKernel with respect to ρ.fst.
Русский
Пусть ρ — конечная мера на β × Ω. Тогда условное ядро константного ядра Kernel.const α ρ совпадает по почти всей мере с ρ.condKernel относительно ρ.fst.
LaTeX
$$$( \\lambda b \\mapsto \\mathrm{condKernel}(\\mathrm{Kernel.const}(\\alpha, \\rho))(a,b) ) =_{\\mathrm{ae}}^{\\rho.fst} \\rho.condKernel$$$
Lean4
theorem condKernel_const [CountableOrCountablyGenerated α β] (ρ : Measure (β × Ω)) [IsFiniteMeasure ρ] (a : α) :
(fun b ↦ Kernel.condKernel (Kernel.const α ρ) (a, b)) =ᵐ[ρ.fst] ρ.condKernel :=
by
have h := Kernel.condKernel_apply_eq_condKernel (Kernel.const α ρ) a
simp_rw [Kernel.fst_apply, Kernel.const_apply] at h
filter_upwards [h] with b hb using hb
