Documentation

Complexity.Probability.UniformNat

Bounded binary indices #

A uniform binary word decodes to a uniform finite index. Capping it puts all excess mass at one sentinel. A power-of-two range above any bound is at most twice the bound plus two, including the zero case.

Main definitions #

Main results #

References #

Adapted from Probability/UniformNat.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

source
def Cslib.Probability.dyadicSize (bound : ℕ) :
ℕ

A power-of-two sampling range strictly larger than the supplied bound.

Instances For
    source
    theorem Cslib.Probability.dyadicSize_pos (bound : ℕ) :
    0 < dyadicSize bound

    The sampling range is positive, including at zero.

    source
    theorem Cslib.Probability.two_le_dyadicSize (bound : ℕ) :
    2 ≤ dyadicSize bound

    Even at zero, the sampler draws at least one fair bit.

    source
    instance Cslib.Probability.instNeZeroNatDyadicSize (bound : ℕ) :
    NeZero (dyadicSize bound)

    The sampling range dyadicSize bound is nonzero.

    source
    theorem Cslib.Probability.lt_dyadicSize (bound : ℕ) :
    bound < dyadicSize bound

    Every index at most the original bound lies in the dyadic range.

    source
    theorem Cslib.Probability.dyadicSize_le (bound : ℕ) :
    dyadicSize bound ≤ 2 * (bound + 1)

    Rounding up to a power of two increases the range by at most a factor of two.

    source
    @[simp]
    theorem Cslib.Probability.dyadicSize_dyadicSize (bound : ℕ) :
    dyadicSize (dyadicSize bound) = 2 * dyadicSize bound

    Applying the rounding operation to a power-of-two range doubles it.

    source
    theorem Cslib.Probability.dyadicSize_polynomiallyBounded :
    PolynomiallyBounded dyadicSize

    The sampling range grows only linearly with its bound.

    source
    theorem Cslib.Probability.dyadicSize_eq_boundedBinaryValue (bound : ℕ) :
    dyadicSize bound = BitString.boundedBinaryValue (2 * bound + 1) (List.replicate (Nat.log 2 bound + 1) true) + 1

    The dyadic range has a bounded unary implementation via the binary decoder.

    source
    theorem Cslib.Probability.uniformFin_decide_lt (size threshold : ℕ) [NeZero size] :
    (PMF.map (fun (i : Fin size) => decide (↑i < threshold)) (PMF.uniformOfFintype (Fin size))) true = ↑(min size threshold) / ↑size

    Comparing a uniform finite index with a threshold samples the corresponding capped fraction.

    source
    theorem Cslib.BitString.uniformList_binaryValue (k : ℕ) :
    PMF.map binaryValue (uniformList k) = PMF.map Fin.val (Probability.PMF.uniformOfFintype (Fin (2 ^ k)))

    Binary decoding identifies fair bit strings with uniform finite indices.

    source
    theorem Cslib.BitString.uniformList_boundedBinaryValue (bound k : ℕ) :
    PMF.map (boundedBinaryValue bound) (uniformList k) = PMF.map (fun (i : Fin (2 ^ k)) => min bound ↑i) (Probability.PMF.uniformOfFintype (Fin (2 ^ k)))

    A capped uniform index can be sampled using exactly k fair bits.