English
If ρ has a disintegration property with respect to a κ, then for almost every x with respect to fst ρ a, the marginal κ(a, x) equals Kernel.condKernel ρ (a, x).
Русский
Если ρ имеет свойство разложения относительно κ, то почти при каждом x по мере fst ρ a имеет место κ(a, x) = Kernel.condKernel ρ (a, x).
LaTeX
$$$\\forall a, \\ ae\\ x \\partial (\\mathrm{Kernel.fst}\\,\\rho\,a), \\ \\kappa(a,x) = \\mathrm{condKernel}(\\rho)(a,x)$$$
Lean4
/-- A finite kernel which satisfies the disintegration property is almost everywhere equal to the
disintegration kernel. -/
theorem eq_condKernel_of_kernel_eq_compProd [CountableOrCountablyGenerated α β] {ρ : Kernel α (β × Ω)}
[IsFiniteKernel ρ] {κ : Kernel (α × β) Ω} [IsFiniteKernel κ] (hκ : Kernel.fst ρ ⊗ₖ κ = ρ) (a : α) :
∀ᵐ x ∂(Kernel.fst ρ a), κ (a, x) = Kernel.condKernel ρ (a, x) :=
by
filter_upwards [Kernel.condKernel_apply_eq_condKernel ρ a,
Kernel.apply_eq_measure_condKernel_of_compProd_eq hκ a] with a h1 h2
rw [h1, h2]
