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 δ} (κ : Kernel α β) (η : Kernel γ δ) : Kernel (α × γ) (β × δ)

Parallel product of two kernels.

Equations

• κ.parallelComp η = (ProbabilityTheory.Kernel.prodMkRight γ κ).prod (ProbabilityTheory.Kernel.prodMkLeft α η)

def ProbabilityTheory.«term_∥ₖ_» : Lean.TrailingParserDescr

Parallel product of two kernels.

Equations

• One or more equations did not get rendered due to their size.

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 δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel γ δ) [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 δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel γ δ) [IsSFiniteKernel η] (ac : α × γ) {g : β × δ → ENNReal} (hg : Measurable g) : ∫⁻ (bd : β × δ), g bd ∂(κ.parallelComp η) ac = ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1

instance ProbabilityTheory.Kernel.instIsSFiniteKernelProdParallelComp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel γ δ) : 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 δ} (κ : Kernel α β) [IsFiniteKernel κ] (η : Kernel γ δ) [IsFiniteKernel η] : 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 δ} (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel γ δ) [IsMarkovKernel η] : 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 δ} (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (η : Kernel γ δ) [IsZeroOrMarkovKernel η] : IsZeroOrMarkovKernel (κ.parallelComp η)

theorem ProbabilityTheory.Kernel.parallelComp_comp_copy {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] : (κ.parallelComp η).comp (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 δ} {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel γ δ} [IsSFiniteKernel η] : (swap β δ).comp (κ.parallelComp η) = (η.parallelComp κ).comp (swap α γ)

theorem ProbabilityTheory.Kernel.deterministic_comp_copy {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) : ((deterministic f hf).parallelComp (deterministic f hf)).comp (copy α) = (copy β).comp (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.