Uniformly random bits on a set of positions

The bits of a uniformly random word ι → Bool on a set S of positions all take a given value with probability 2 ^ (-|S|) (BitString.expect_ite_forall_mem_eq), by the count of words agreeing off a set (BitString.card_filter_forall_notMem_eq).

Main results

• Cslib.BitString.expect_ite_forall_mem_eq: a set of k uniformly random bits takes a given value with probability 2 ^ (-k).

theorem Cslib.BitString.expect_ite_forall_mem_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (b : Bool) [DecidablePred fun (x : ι → Bool) => ∀ i ∈ S, x i = b] : (Finset.univ.expect fun (x : ι → Bool) => if ∀ i ∈ S, x i = b then 1 else 0) = 2⁻¹ ^ S.card

The bits of a set S of uniformly random bits are all equal to b with probability 2 ^ (-|S|), for any decision procedure of the event.