English
For ρ with κ and hκ: ρ = ρ.fst.compProd κ implies κ x = ρ.condKernel x for a.e. x.
Русский
Для ρ с κ и hκ: ρ = ρ.fst.compProd κ значит, что x-отκ равно ρ.condKernel x почти всюду.
LaTeX
$$$Eq\\(ρ.fst.compProd κ\\,Ω\\) \\\\rightarrow \\forall x, \\ κ x = ρ.condKernel x \\text{ a.e. } x$$$
Lean4
/-- A s-finite kernel which satisfy the disintegration property of the given measure `ρ` is almost
everywhere equal to the disintegration kernel of `ρ` when evaluated on a measurable set.
This theorem in the case of finite kernels is weaker than `eq_condKernel_of_measure_eq_compProd`
which asserts that the kernels are equal almost everywhere and not just on a given measurable
set. -/
theorem eq_condKernel_of_measure_eq_compProd' (κ : Kernel α Ω) [IsSFiniteKernel κ] (hκ : ρ = ρ.fst ⊗ₘ κ) {s : Set Ω}
(hs : MeasurableSet s) : ∀ᵐ x ∂ρ.fst, κ x s = ρ.condKernel x s :=
by
refine
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (Kernel.measurable_coe κ hs) (Kernel.measurable_coe ρ.condKernel hs)
(fun t ht _ ↦ ?_)
conv_rhs => rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]
simp only [Measure.compProd_apply (ht.prod hs), ← lintegral_indicator ht]
congr with x
by_cases hx : x ∈ t <;> simp [hx]
