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
Notations #
κ ∥ₖ η = 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 γ δ)
:
Parallel product of two kernels.
Equations
- κ.parallelComp η = if h : ProbabilityTheory.IsSFiniteKernel κ ∧ ProbabilityTheory.IsSFiniteKernel η then { toFun := fun (x : α × γ) => (κ x.1).prod (η x.2), measurable' := ⋯ } else 0
Instances For
Parallel product of two kernels.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 κ)
:
@[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 η)
:
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 : α × γ)
:
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)
:
@[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 η]
:
@[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 γ δ)
:
@[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 α β)
:
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)
:
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)
:
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 γ δ)
:
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)]
:
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 η]
:
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 η)