Conjecture Decidable Sampling [efr-HII6]

Let \mathcal {C} be an elementary topos with natural numbers object, and let \mathcal {C} \to \mathcal {C}_s be a Markov promonad which is compatible with the natural numbers object, pullbacks along monomorphisms and (internal) sequential inverse limits, and which has a fair coinflip \operatorname {cf}. Let [0,1] denote the interval in the Dedekind reals in \mathrm {cc}. Let \operatorname {cf}^\mathbb {N} : * \to 2^\mathbb {N} be as usual the IID coupling of fair coinflips, and consider the map in \mathcal {C}_s.

[0,1] \xrightarrow {[0,1] \otimes \operatorname {cf}^\mathbb {N}} [0,1] \otimes 2^\mathbb {N} \xrightarrow {[0,1] \otimes p} [0,1] \otimes [0,1] \xrightarrow {>} \Omega

which first draws an IID sample, then interprets the sequence as a real, then compares it with the given value. Then this map factors over the inclusion 2 \to \Omega .

Backlinks

Related