Theorems · Definition · probability

ProbabilityTheory.Kernel.parallelComp

{α : Type u_5} →
  {β : Type u_6} →
    {γ : Type u_7} →
      {δ : Type u_8} →
        {mα : MeasurableSpace α} →
          {mβ : MeasurableSpace β} →
            {mγ : MeasurableSpace γ} →
              {mδ : MeasurableSpace δ} →
                ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel γ δ → ProbabilityTheory.Kernel (α × γ) (β × δ)

Parallel product of two kernels.

Defined in: Mathlib.Probability.Kernel.Composition.ParallelComp
Cited by: 49 results in Mathlib
Foundations: Depth 220 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.

Cites2

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

MeasurableSpacestatement · cited by 13,106
ProbabilityTheory.Kernelstatement · cited by 1,281

Cited by52

Results whose statement or proof uses this declaration.

ProbabilityTheory.Kernel.prodproof · cited by 65
ProbabilityTheory.Kernel.compProd_applyproof · cited by 31
ProbabilityTheory.Kernel.parallelComp_applystatement · cited by 18
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_leftproof · cited by 12
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_rightproof · cited by 8
ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_leftstatement · cited by 7
ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_rightstatement · cited by 7
ProbabilityTheory.Kernel.prod_apply'proof · cited by 6
ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelCompstatement and proof · cited by 5
ProbabilityTheory.Kernel.compProd_defstatement and proof · cited by 5
ProbabilityTheory.Kernel.swap_parallelCompstatement and proof · cited by 4
MeasureTheory.Measure.compProd_mapproof · cited by 4