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

Notation

• κ ∥ₖ η = ProbabilityTheory.Kernel.parallelComp κ η

theorem ProbabilityTheory.Kernel.parallelComp_def {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel γ δ) : κ.parallelComp η = if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then { toFun := fun (x : α × γ) => (κ x.1).prod (η x.2), measurable' := ⋯ } else 0

@[irreducible]

noncomputable def ProbabilityTheory.Kernel.parallelComp {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) (η : Kernel γ δ) : Kernel (α × γ) (β × δ)

Parallel product of two kernels.

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

Parallel product of two kernels.

@[simp]

theorem ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : Kernel α β} (η : Kernel γ δ) (h : ¬IsSFiniteKernel κ) : κ.parallelComp η = 0

@[simp]

theorem ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {η : Kernel γ δ} (κ : Kernel α β) (h : ¬IsSFiniteKernel η) : κ.parallelComp η = 0

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.parallelComp_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : Kernel α β} {η : Kernel γ δ} {x : α × γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set (β × δ)} (hs : MeasurableSet s) : ((κ.parallelComp η) x) s = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1

theorem ProbabilityTheory.Kernel.parallelComp_apply_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : Kernel α β} {η : Kernel γ δ} {x : α × γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] (s : Set β) (t : Set δ) : ((κ.parallelComp η) x) (s ×ˢ t) = (κ x.1) s * (η x.2) t

@[simp]

theorem ProbabilityTheory.Kernel.parallelComp_apply_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : Kernel α β} {η : Kernel γ δ} {x : α × γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] : ((κ.parallelComp η) x) Set.univ = (κ x.1) Set.univ * (η x.2) Set.univ

@[simp]

theorem ProbabilityTheory.Kernel.parallelComp_zero_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (η : Kernel γ δ) : parallelComp 0 η = 0

@[simp]

theorem ProbabilityTheory.Kernel.parallelComp_zero_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : Kernel α β) : κ.parallelComp 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.id_parallelComp_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : Kernel.id.parallelComp Kernel.id = Kernel.id

theorem ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) : (deterministic f hf).parallelComp (deterministic g hg) = deterministic (Prod.map f g) ⋯

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

theorem ProbabilityTheory.Kernel.lintegral_parallelComp_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : Kernel α β} {η : Kernel γ δ} [IsSFiniteKernel κ] [IsSFiniteKernel η] (ac : α × γ) {g : β × δ → ENNReal} (hg : Measurable g) : ∫⁻ (bd : β × δ), g bd ∂(κ.parallelComp η) ac = ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂κ ac.1 ∂η ac.2

theorem ProbabilityTheory.Kernel.parallelComp_sum_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {ι : Type u_5} [Countable ι] (κ : ι → Kernel α β) [∀ (i : ι), IsSFiniteKernel (κ i)] (η : Kernel γ δ) : (Kernel.sum κ).parallelComp η = Kernel.sum fun (i : ι) => (κ i).parallelComp η

theorem ProbabilityTheory.Kernel.parallelComp_sum_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {ι : Type u_5} [Countable ι] (κ : Kernel α β) (η : ι → Kernel γ δ) [∀ (i : ι), IsSFiniteKernel (η i)] : κ.parallelComp (Kernel.sum η) = Kernel.sum fun (i : ι) => κ.parallelComp (η i)

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 α β} {η : Kernel γ δ} [IsMarkovKernel κ] [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 α β} {η : Kernel γ δ} [IsZeroOrMarkovKernel κ] [IsZeroOrMarkovKernel η] : IsZeroOrMarkovKernel (κ.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 α β} {η : Kernel γ δ} [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ.parallelComp η)

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 η)