Theorems · Theorem · probability

ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal

∀ {α : 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 Ω η) = κ

For κ' := map κ (Prod.map (id : β → β) e), the hypothesis hη is fst κ' ⊗ₖ η = κ'. With that hypothesis, fst κ ⊗ₖ borelMarkovFromReal κ η = κ.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel