Theorems · Definition · probability

ProbabilityTheory.Kernel.prodMkRight

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (γ : Type u_5) → [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel (α × γ) β

Define a Kernel (α × γ) β from a Kernel α β by taking the comap of the projection.

Defined in: Mathlib.Probability.Kernel.Composition.MapComap
Cited by: 18 results in Mathlib
Foundations: Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
measurable_fstproof · cited by 79
ProbabilityTheory.Kernel.comapproof · cited by 34

Cited by18

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.sectL_prodMkRightstatement · cited by 1
ProbabilityTheory.Kernel.prodMkRight_applystatement · cited by 1
ProbabilityTheory.Kernel.prodMkRight_zerostatement · cited by 1
ProbabilityTheory.Kernel.prod_prodMkRight_comp_deterministic_prodstatement and proof · cited by 1
ProbabilityTheory.Kernel.lintegral_prodMkRightstatement · cited by 0
ProbabilityTheory.Kernel.sectR_prodMkRightstatement · cited by 0
ProbabilityTheory.Kernel.sum_prodMkRightstatement · cited by 0
ProbabilityTheory.Kernel.swapLeft_prodMkLeftstatement · cited by 0
ProbabilityTheory.Kernel.swapLeft_prodMkRightstatement · cited by 0
ProbabilityTheory.Kernel.comap_prod_swapstatement and proof · cited by 0
ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRightstatement and proof · cited by 0
ProbabilityTheory.Kernel.prodMkRight_addstatement and proof · cited by 0