Inner products of bit strings as parities

Over the two-element Boolean ring, the inner product x ⬝ᵥ w = Σᵢ xᵢ wᵢ of two bit strings is the parity of x on the support of w (Cslib.BitString.dotProduct_eq_parityOn). Parities on nonempty sets are balanced (Cslib.card_filter_parityOn_eq), so the inner product with a fixed nonzero string takes each value on half of the strings.

Main results

• Cslib.BitString.dotProduct_eq_parityOn: the inner product with w is the parity on the support of w.

theorem Cslib.BitString.dotProduct_eq_parityOn {ι : Type u_1} [Fintype ι] (x w : ι → Bool) : x ⬝ᵥ w = parityOn {i : ι | w i = true} x

The inner product with w is the parity on the support of w.