Statistical Kernel Transcript Invariance

Abstract

Equal kernel laws give equal randomized transcript laws.

Theorem 1.1 (Equal kernel laws generate equal transcript laws).

$$\begin{array}{c}\forall X,O,R,D:\mathrm{Type},\\ [\mathrm{MeasurableSpace}(X)],[\mathrm{MeasurableSpace}(O)],[\mathrm{MeasurableSpace}(R)],[\mathrm{MeasurableSpace}(D)],\\ K:\mathrm{Kernel}\left(X,O\right),\mathrm{Markov}\left(K\right),\\ x,y:X,K(x)=K(y)\Rightarrow \\ \forall n\in \mathbb{N},P:\mathrm{Kernel}\left(\mathrm{Fin}\left(n\right)\to O,R\right),\mathrm{Markov}\left(P\right),\\ A:\mathrm{Kernel}\left(R,D\right),\mathrm{Markov}\left(A\right),\\ \mathrm{bind}\left(\mathrm{bind}\left(\mathrm{ProductMeasure}\left(\mathrm{Fin}\left(n\right),K(x)\right),P\right),A\right)=\mathrm{bind}\left(\mathrm{bind}\left(\mathrm{ProductMeasure}\left(\mathrm{Fin}\left(n\right),K(y)\right),P\right),A\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/KernelTranscriptInvariance.statistical_kernel_transcript_law_invariant (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hypothesis is equality of the two probability measures returned by the same Markov channel at x and y. For each public sample count n, the input transcript law is the canonical finite product of that channel measure, including the zero-sample product.

The public kernels P and A respectively model arbitrary Markov postprocessing and a randomized decision rule. Composing both with the finite product laws constructs the final transcript laws rather than defining a transcript to have the desired equality.

Measure equality is preserved first by the finite product constructor and then by both measure-kernel compositions, which yields the displayed equality for every sample count and both processors.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/KernelTranscriptInvariance.statistical_kernel_transcript_law_invariant