English
In the Real-case variant, the same almost-everywhere equality holds for real-valued kernels.
Русский
В случае Real сохраняется почти всюду тождество для реал-ядра.
LaTeX
$$$eq\\_condKernel\\_of\\_measure\\_eq\\_compProd\\_real$$$
Lean4
/-- Auxiliary lemma for `eq_condKernel_of_measure_eq_compProd`.
Uniqueness of the disintegration kernel on ℝ. -/
theorem eq_condKernel_of_measure_eq_compProd_real {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ] (κ : Kernel α ℝ)
[IsFiniteKernel κ] (hκ : ρ = ρ.fst ⊗ₘ κ) : ∀ᵐ x ∂ρ.fst, κ x = ρ.condKernel x :=
by
have huniv : ∀ᵐ x ∂ρ.fst, κ x Set.univ = ρ.condKernel x Set.univ :=
eq_condKernel_of_measure_eq_compProd' κ hκ MeasurableSet.univ
suffices ∀ᵐ x ∂ρ.fst, ∀ ⦃t⦄, MeasurableSet t → κ x t = ρ.condKernel x t
by
filter_upwards [this] with x hx
ext t ht; exact hx ht
apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat Real.isPiSystem_Iic_rat
· simp
· simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
exact ae_all_iff.2 fun q ↦ eq_condKernel_of_measure_eq_compProd' κ hκ measurableSet_Iic
· filter_upwards [huniv] with x hxuniv t ht heq
rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _]
· refine ae_of_all _ (fun x f hdisj hf heq ↦ ?_)
rw [measure_iUnion hdisj hf, measure_iUnion hdisj hf]
exact tsum_congr heq
