Hitting a fixed target through a bijection #
A uniformly sampled value, pushed through a bijection, hits any fixed target with probability
1 / |domain|.
theorem
Cryptlib.Util.UniformHit.uniformHit_eq_of_injective
{F G : Type}
[Fintype F]
[SampleableType F]
[DecidableEq G]
{act : F → G}
(hinj : Function.Injective act)
{target : G}
(htarget : target ∈ Set.range act)
:
A uniformly sampled b : F, pushed through an injective act, hits any target in its image
with probability 1/|F|.
theorem
Cryptlib.Util.UniformHit.uniformHit_eq
{F G : Type}
[Fintype F]
[SampleableType F]
[DecidableEq G]
{act : F → G}
(hact : Function.Bijective act)
(target : G)
:
A uniformly sampled b : F, pushed through a bijection act, hits any fixed target with
probability 1/|F|.