Theorems · Theorem · probability

ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd

∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) ℝ) [ProbabilityTheory.IsSFiniteKernel η],
  (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η =
      κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) →
    κ.fst.compProd (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) =
      ((κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η).comapRight ⋯

For κ' := map κ (Prod.map (id : β → β) e), the hypothesis hη is fst κ' ⊗ₖ η = κ'. The conclusion of the lemma is fst κ ⊗ₖ borelMarkovFromReal Ω η = comapRight (fst κ' ⊗ₖ η) _.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

1 results in Mathlib

Foundations

Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

StandardBorelSpaceNonemptyProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel