Acceptance of independent fixed-width blocks

Splitting a uniform word into equal-width rows gives independent uniform samples. Testing every row therefore multiplies the individual acceptance probabilities, including zero rows or width.

Main results

• Cslib.BitString.uniformList_all_listRow_true: the exact acceptance probability of repeated fixed-width Boolean checks.

theorem Cslib.BitString.uniformList_all_listRow_true (count width : ℕ) (check : List Bool → Bool) : (PMF.map (fun (word : List Bool) => (List.range count).all fun (i : ℕ) => check (listRow width i word)) (uniformList (count * width))) true = (PMF.map check (uniformList width)) true ^ count

Every fixed-width check accepts with the product probability of independent uniform rows.