The parity function

parityOn s x says whether an odd number of the bits of x : ι → Bool in s are true, and parity n is the parity of all n bits. These are the parity functions χ_S of O'Donnell, Chapter 1, with values in Bool rather than ±1.

In the Boolean ring Bool, where a + b = (a ^^ b), the parity on s is the sum of the bits in s (parityOn_eq_sum), so it splits over disjoint unions (parityOn_union), the parity on a symmetric difference is the exclusive or of the parities (parityOn_symmDiff), and it is additive for the coordinatewise sum of bit strings (parityOn_add, bundled as parityOnAddMonoidHom). Bit strings are added with +, under which each is its own negative (BooleanRing.add_self), and single bits with ^^. Flipping one of the bits negates the parity (parityOn_update_not), so the parity of a nonempty set of bits is not constant and depends on each of them; being additive, it then takes each value on exactly half of the inputs (card_filter_parityOn_eq).

Main definitions

• Cslib.parityOn: the parity of the bits in a set, and Cslib.parityOnAddMonoidHom the same as an additive map.
• Cslib.parity: the parity of all bits.

Main results

• Cslib.parityOn_eq_sum: the parity is the sum of the bits in the Boolean ring.
• Cslib.parityOn_singleton: the parity on a singleton {i} is x i.
• Cslib.parityOn_union, Cslib.parityOn_sdiff, Cslib.parityOn_biUnion: the parity of a disjoint union, set difference, and disjoint indexed union.
• Cslib.parityOn_symmDiff: the parity of a symmetric difference.
• Cslib.parityOn_add, Cslib.BitString.exists_eq_parityOn_iff: the parities are the linear Boolean functions.
• Cslib.parity_update_not: flipping any bit flips the parity.
• Cslib.card_filter_parityOn_eq, Cslib.dens_filter_parityOn_eq: the parity on a nonempty set takes each value on half of the inputs.
• Cslib.card_filter_parity_eq_true: parity of n ≥ 1 bits is true on 2 ^ (n - 1) inputs.
• Cslib.foldl_bne_eq_parity: folding xor (bne) over a list of bits computes parity.

References

• R. O'Donnell, Analysis of Boolean Functions

def Cslib.parityOn {ι : Type u_1} (s : Finset ι) (x : ι → Bool) : Bool

The parity of the bits of x in s: whether an odd number of them are true.

def Cslib.parity (n : ℕ) : BooleanFunction n

The parity function on n bits.

theorem Cslib.parityOn_eq_sum {ι : Type u_1} (s : Finset ι) (x : ι → Bool) : parityOn s x = ∑ i ∈ s, x i

The parity is the sum of the bits in the Boolean ring Bool.

@[simp]

theorem Cslib.parityOn_empty {ι : Type u_1} (x : ι → Bool) : parityOn ∅ x = false

The parity on the empty set is false.

@[simp]

theorem Cslib.parityOn_singleton {ι : Type u_1} (i : ι) (x : ι → Bool) : parityOn {i} x = x i

The parity on a singleton {i} is the bit x i.

theorem Cslib.parityOn_congr {ι : Type u_1} {s : Finset ι} {x y : ι → Bool} (h : ∀ j ∈ s, x j = y j) : parityOn s x = parityOn s y

The parity on s only reads the bits in s.

theorem Cslib.parityOn_add {ι : Type u_1} (S : Finset ι) (x y : ι → Bool) : parityOn S (x + y) = (parityOn S x ^^ parityOn S y)

Parities are linear: the parity of a sum of bit strings is the exclusive or of the parities.

def Cslib.parityOnAddMonoidHom {ι : Type u_1} (s : Finset ι) : (ι → Bool) →+ Bool

The parity on s, as an additive map from bit strings to bits.

@[simp]

theorem Cslib.parityOnAddMonoidHom_apply {ι : Type u_1} (s : Finset ι) (x : ι → Bool) : (parityOnAddMonoidHom s) x = parityOn s x

parityOnAddMonoidHom s evaluates to parityOn s.

theorem Cslib.parityOn_insert {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i : ι} (hi : i ∉ s) (x : ι → Bool) : parityOn (insert i s) x = (x i ^^ parityOn s x)

Adding a new position i ∉ s to the set exclusive-ors the bit x i into the parity.

theorem Cslib.parityOn_eq_xor_erase {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i : ι} (hi : i ∈ s) (x : ι → Bool) : parityOn s x = (x i ^^ parityOn (s.erase i) x)

For i ∈ s, the parity on s is x i exclusive-or the parity on s.erase i.

theorem Cslib.parityOn_update_of_notMem {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i : ι} (hi : i ∉ s) (x : ι → Bool) (b : Bool) : parityOn s (Function.update x i b) = parityOn s x

Changing a bit outside s does not change the parity on s.

theorem Cslib.parityOn_union {ι : Type u_1} [DecidableEq ι] {s t : Finset ι} (h : Disjoint s t) (x : ι → Bool) : parityOn (s ∪ t) x = (parityOn s x ^^ parityOn t x)

The parity of a disjoint union is the exclusive or of the parities.

theorem Cslib.parityOn_sdiff {ι : Type u_1} [DecidableEq ι] {s t : Finset ι} (h : s ⊆ t) (x : ι → Bool) : parityOn (t \ s) x = (parityOn t x ^^ parityOn s x)

The parity on a set difference t \ s for s ⊆ t is the exclusive or of the parities.

theorem Cslib.parityOn_symmDiff {ι : Type u_1} [DecidableEq ι] (s t : Finset ι) (x : ι → Bool) : parityOn (symmDiff s t) x = (parityOn s x ^^ parityOn t x)

The parity on a symmetric difference is the exclusive or of the parities: the bits in both sets are counted twice.

theorem Cslib.parityOn_biUnion {ι : Type u_1} [DecidableEq ι] {κ : Type u_2} {S : Finset κ} {B : κ → Finset ι} (hB : (↑S).PairwiseDisjoint B) (x : ι → Bool) : parityOn (S.biUnion B) x = parityOn S fun (j : κ) => parityOn (B j) x

The parity of a union of pairwise disjoint blocks is the parity of the parities of the blocks.

theorem Cslib.parityOn_update_not {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i : ι} (hi : i ∈ s) (x : ι → Bool) : parityOn s (Function.update x i !x i) = !parityOn s x

Flipping one of the bits negates the parity.

theorem Cslib.parity_update_not {n : ℕ} (x : BitString n) (i : Fin n) : parity n (Function.update x i !x i) = !parity n x

Flipping any bit flips the parity.

theorem Cslib.card_filter_parityOn_eq {ι : Type u_1} [DecidableEq ι] {s : Finset ι} [Fintype ι] (hs : s.Nonempty) (b : Bool) : {x : ι → Bool | parityOn s x = b}.card = 2 ^ (Fintype.card ι - 1)

Parities of nonempty sets are balanced: the parity on a nonempty set of bits takes each value on half of the inputs. Being additive, it has fibers of equal size.

theorem Cslib.dens_filter_parityOn_eq {ι : Type u_1} [DecidableEq ι] {s : Finset ι} [Fintype ι] (hs : s.Nonempty) (b : Bool) : {x : ι → Bool | parityOn s x = b}.dens = 2⁻¹

Parities of nonempty sets are balanced: the parity on a nonempty set of bits takes each value with probability one half at a uniformly random input.

theorem Cslib.card_filter_parity_eq_true {n : ℕ} (hn : 1 ≤ n) : {x : BitString n | parity n x = true}.card = 2 ^ (n - 1)

Parity of n ≥ 1 bits is true on half of the inputs.

theorem Cslib.card_filter_parity_eq_false {n : ℕ} (hn : 1 ≤ n) : {x : BitString n | parity n x = false}.card = 2 ^ (n - 1)

Parity of n ≥ 1 bits is false on half of the inputs.

theorem Cslib.not_dependsOn_parityOn {ι : Type u_1} {s : Finset ι} {i : ι} (hi : i ∈ s) (c : Bool) : ¬DependsOn (fun (x : ι → Bool) => c ^^ parityOn s x) {i}ᶜ

The parity, possibly negated, depends on each of its bits.

theorem Cslib.not_isConst_parityOn {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) (c : Bool) : ¬Function.IsConst fun (x : ι → Bool) => c ^^ parityOn s x

The parity of a nonempty set of bits, possibly negated, is not constant.

theorem Cslib.BitString.exists_eq_parityOn_iff {ι : Type u_1} [Finite ι] {f : (ι → Bool) → Bool} : (∃ (S : Finset ι), f = parityOn S) ↔ ∀ (x y : ι → Bool), f (x + y) = (f x ^^ f y)

The linear Boolean functions are the parities: a Boolean function turns sums of bit strings into the exclusive or of its values exactly when it is the parity of some set of coordinates O'Donnell, Definition 1.28.

theorem Cslib.foldl_bne_eq_parity (w : List Bool) : List.foldl bne false w = parity w.length fun (i : Fin w.length) => w[i]

Folding xor over a Boolean word computes parity of its slice.