condDistrib_ae_eq_iff_measure_eq_compProd

English

If X is measurable and Y is measurable, then condDistrib Y X μ equals the a.e. unique kernel κ satisfying μ.map (X, Y) = μ.map X ⊗ κ.

Русский

Если X и Y измеримы, то condDistrib Y X μ равно почти наверняка едиственному ядру κ, удовлетворяющему μ.map (X,Y) = μ.map X ⊗ κ.

LaTeX

$$$$ \\mathrm{condDistrib}(Y,X,μ) =_{a.e.} κ \\text{ where } μ.map (X,Y) = μ.map X ⊗ κ.$$$$

Lean4

theorem condDistrib_ae_eq_iff_measure_eq_compProd (X : α → β) (hY : AEMeasurable Y μ) (κ : Kernel β Ω)
    [IsFiniteKernel κ] : (condDistrib Y X μ =ᵐ[μ.map X] κ) ↔ μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ :=
  by
  refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd X hY⟩
  rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY]

Похожие утверждения