Parallel composition of kernels #
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)
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 η)
Equations
- ⋯ = ⋯
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 η)
Equations
- ⋯ = ⋯
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 η)
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.Kernel.prod_eq_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 η]
:
κ.prod η = (κ.parallelComp η).comp (ProbabilityTheory.Kernel.copy α)
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.measurable_Kernel_prod_mk_left''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{t : Set (γ × β)}
(ht : MeasurableSet t)
:
Measurable (Function.uncurry fun (a : α) (y : γ) => (κ a) (Prod.mk y ⁻¹' t))
@[simp]
theorem
ProbabilityTheory.Kernel.swap_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{η : ProbabilityTheory.Kernel α γ}
[ProbabilityTheory.IsSFiniteKernel η]
:
(ProbabilityTheory.Kernel.swap β γ).comp (κ.prod η) = η.prod κ