Theorems · Theorem · probability

ProbabilityTheory.Kernel.swap_parallelComp

∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y}
  {η : ProbabilityTheory.Kernel Z T},
  (ProbabilityTheory.Kernel.swap Y T).comp (κ.parallelComp η) =
    (η.parallelComp κ).comp (ProbabilityTheory.Kernel.swap X Z)

Defined in: Mathlib.Probability.Kernel.Composition.KernelLemmas
Cited by: 4 results in Mathlib
Foundations: Depth 226 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites41

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

DFunLike.coeproof · cited by 62,936
Setproof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measureproof · cited by 10,939
ENNRealproof · cited by 9,879
Set.preimageproof · cited by 4,946
MeasurableSetproof · cited by 3,075
one_mulproof · cited by 2,841
ProbabilityTheory.Kernelstatement and proof · cited by 1,281
MeasureTheory.lintegralproof · cited by 1,152
MeasureTheory.Measure.prodproof · cited by 353
MeasureTheory.Measure.extproof · cited by 308

Cited by4

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelCompproof · cited by 2
ProbabilityTheory.parallelProd_posterior_comp_copy_compproof · cited by 2
ProbabilityTheory.posterior_compproof · cited by 0
MeasureTheory.Measure.prod_comp_leftproof · cited by 0