condKernel_compProd — Mathlib

English

If ρ = ρ.fst.compProd κ, then for almost every a, the conditional kernel κ a equals ρ.condKernel a.

Русский

Если ρ = ρ.fst.compProd κ, то почти наверху a выполнено κ a = ρ.condKernel a.

LaTeX

$$$Eq (ρ.fst.compProd κ) ρ \\rightarrow \\forall a, κ a = ρ.condKernel a$$$

Lean4

theorem condKernel_compProd (μ : Measure α) [IsFiniteMeasure μ] (κ : Kernel α Ω) [IsMarkovKernel κ] :
    (μ ⊗ₘ κ).condKernel =ᵐ[μ] κ :=
  by
  suffices κ =ᵐ[(μ ⊗ₘ κ).fst] (μ ⊗ₘ κ).condKernel by symm; rwa [Measure.fst_compProd] at this
  refine eq_condKernel_of_measure_eq_compProd _ ?_
  rw [Measure.fst_compProd]

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