Parallel composition of kernels #
Two kernels κ : Kernel α β and η : Kernel γ δ can be applied in parallel to give a kernel
κ ∥ₖ η from α × γ to β × δ: (κ ∥ₖ η) (a, c) = (κ a).prod (η c).
Main definitions #
parallelComp (κ : Kernel α β) (η : Kernel γ δ) : Kernel (α × γ) (β × δ): parallel composition of two s-finite kernels. We define a notationκ ∥ₖ η = parallelComp κ η.∫⁻ bd, g bd ∂(κ ∥ₖ η) ac = ∫⁻ b, ∫⁻ d, g (b, d) ∂η ac.2 ∂κ ac.1
Main statements #
parallelComp_comp_copy:(κ ∥ₖ η) ∘ₖ (copy α) = κ ×ₖ ηdeterministic_comp_copy: for a deterministic kernel, copying then applying the kernel to the two copies is the same as first applying the kernel then copying. That is, ifκis a deterministic kernel,(κ ∥ₖ κ) ∘ₖ copy α = copy β ∘ₖ κ.
Notations #
κ ∥ₖ η = ProbabilityTheory.Kernel.parallelComp κ η
Implementation notes #
Our formalization of kernels is centered around the composition-product: the product and then the
parallel composition are defined as special cases of the composition-product.
We could have alternatively used the building blocks of kernels seen as a Markov category:
composition, parallel composition (or tensor product) and the deterministic kernels id, copy,
swap and discard. The product and composition-product could then be built from these.
noncomputable def
ProbabilityTheory.Kernel.parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel γ δ)
:
ProbabilityTheory.Kernel (α × γ) (β × δ)
Parallel product of two kernels.
Equations
- κ.parallelComp η = (ProbabilityTheory.Kernel.prodMkRight γ κ).prod (ProbabilityTheory.Kernel.prodMkLeft α η)
Instances For
Parallel product of two kernels.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.Kernel.parallelComp_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsSFiniteKernel η]
(x : α × γ)
:
(κ.parallelComp η) x = (κ x.1).prod (η x.2)
theorem
ProbabilityTheory.Kernel.lintegral_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsSFiniteKernel η]
(ac : α × γ)
{g : β × δ → ENNReal}
(hg : Measurable g)
:
instance
ProbabilityTheory.Kernel.instIsSFiniteKernelProdParallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel γ δ)
:
ProbabilityTheory.IsSFiniteKernel (κ.parallelComp η)
instance
ProbabilityTheory.Kernel.instIsFiniteKernelProdParallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.IsFiniteKernel (κ.parallelComp η)
instance
ProbabilityTheory.Kernel.instIsMarkovKernelProdParallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.IsMarkovKernel (κ.parallelComp η)
instance
ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdParallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(η : ProbabilityTheory.Kernel γ δ)
[ProbabilityTheory.IsZeroOrMarkovKernel η]
:
ProbabilityTheory.IsZeroOrMarkovKernel (κ.parallelComp η)
theorem
ProbabilityTheory.Kernel.parallelComp_comp_copy
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsSFiniteKernel η]
:
(κ.parallelComp η).comp (ProbabilityTheory.Kernel.copy α) = κ.prod η
theorem
ProbabilityTheory.Kernel.swap_parallelComp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel γ δ}
[ProbabilityTheory.IsSFiniteKernel η]
:
(ProbabilityTheory.Kernel.swap β δ).comp (κ.parallelComp η) = (η.parallelComp κ).comp (ProbabilityTheory.Kernel.swap α γ)
theorem
ProbabilityTheory.Kernel.deterministic_comp_copy
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
:
((ProbabilityTheory.Kernel.deterministic f hf).parallelComp (ProbabilityTheory.Kernel.deterministic f hf)).comp
(ProbabilityTheory.Kernel.copy α) = (ProbabilityTheory.Kernel.copy β).comp (ProbabilityTheory.Kernel.deterministic f hf)
For a deterministic kernel, copying then applying the kernel to the two copies is the same as first applying the kernel then copying.