Class IsDeterministic of deterministic kernels

This file defines the class IsDeterministic of deterministic kernels, and proves some properties about them.

Main definitions

• Kernel.IsDeterministic: a kernel is deterministic if copying then applying the kernel to the two copies is the same as first applying the kernel then copying.

Main statements

• isDeterministic_iff_isZeroOneMeasure: a finite kernel is deterministic if and only if it is a zero-one measure for every input.
• IsDeterministic.exists_eq_deterministic: in a standard Borel space, a deterministic Markov kernel is a Dirac kernel of some measurable function.
• comp_parallelComp_comp_copy: if the composition of two Markov kernels η ∘ₖ κ is deterministic, the distribution over both η ∘ₖ κ and κ can be obtained by computing η ∘ₖ κ and κ independently. This corresponds to the equation of a Positive Markov category. See Example 11.25 of [Fri20].

Implementation notes

comp_parallelComp_comp_copy is true only when considering Markov kernels. To see why, consider the counterexample with $X = Y = \{\varnothing\}$, kernels $\kappa(\cdot | \varnothing) = 2\delta_ {\varnothing}$ and $\eta(\cdot | \varnothing) = (1/2)\delta_{\varnothing}$: although their composition is deterministic, the equation fails.

References

• A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics
• Moss and Perrone, A category-theoretic proof of the ergodic decomposition theorem

class ProbabilityTheory.IsDeterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : Prop

A kernel is deterministic if copying then applying the kernel to the two copies is the same as first applying the kernel then copying.

• parallelComp_self_comp_copy' : (κ.parallelComp κ).comp (Kernel.copy α) = (Kernel.copy β).comp κ

theorem ProbabilityTheory.Kernel.parallelComp_self_comp_copy {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : Kernel α β} [IsDeterministic κ] : (κ.parallelComp κ).comp (copy α) = (copy β).comp κ

instance ProbabilityTheory.Kernel.instIsDeterministicDeterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) : IsDeterministic (deterministic f hf)

instance ProbabilityTheory.Kernel.instIsDeterministicId {α : Type u_1} {mα : MeasurableSpace α} : IsDeterministic Kernel.id

instance ProbabilityTheory.Kernel.instIsDeterministicProdCopy {α : Type u_1} {mα : MeasurableSpace α} : IsDeterministic (copy α)

instance ProbabilityTheory.Kernel.instIsDeterministicPUnitDiscard {α : Type u_1} {mα : MeasurableSpace α} : IsDeterministic (discard α)

instance ProbabilityTheory.Kernel.instIsDeterministicProdSwap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} : IsDeterministic (swap α β)

theorem ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsFiniteKernel κ] : IsDeterministic κ ↔ ∀ (a : α), MeasureTheory.IsZeroOneMeasure (κ a)

instance ProbabilityTheory.Kernel.instIsZeroOneMeasureCoeMeasureOfIsFiniteKernelOfIsDeterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [IsFiniteKernel κ] [IsDeterministic κ] (a : α) : MeasureTheory.IsZeroOneMeasure (κ a)

theorem ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [StandardBorelSpace β] (κ : Kernel α β) [IsMarkovKernel κ] [IsDeterministic κ] : ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf

in a standard Borel space, a deterministic Markov kernel is a Dirac kernel of one measurable function.

theorem ProbabilityTheory.Kernel.comp_parallelComp_comp_copy {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} [MeasurableSpace γ] {κ : Kernel α β} {η : Kernel β γ} [IsMarkovKernel κ] [IsMarkovKernel η] [IsDeterministic (η.comp κ)] : ((η.comp κ).parallelComp κ).comp (copy α) = ((η.parallelComp Kernel.id).comp (copy β)).comp κ

The equation of a Positive Markov category: if the composition of two Markov kernels η ∘ₖ κ is deterministic, the distribution over both η ∘ₖ κ and κ can be obtained by computing η ∘ₖ κ and κ independently.