Combining independent uniform draws #
A bijective binary operation transports two independent uniform draws to a uniform draw. The operation's codomain can carry its own measurable structure.
theorem
evalDist_seq_map_eq_uniformOn
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
[EvalDistSemantics m]
[LawfulEvalDistSemantics m]
{α β γ : Type u}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[MeasurableSingletonClass γ]
[Finite α]
[Finite β]
[Nonempty α]
[Nonempty β]
(mx : m α)
(my : m β)
(f : α → β → γ)
(hx : 𝒟[mx] = ProbabilityTheory.uniformOn Set.univ)
(hy : 𝒟[my] = ProbabilityTheory.uniformOn Set.univ)
(hf : Measurable (Function.uncurry f))
(hbij : Function.Bijective (Function.uncurry f))
:
A measurable bijective combination of independent finite uniform draws is uniform.