Threshold, majority and symmetric Boolean functions

The threshold function threshold n j says that at least j of n bits are true, and majority (majority, at least half) and strict majority (strictMajority, more than half) are threshold functions. On an arbitrary finite set of voting indices, BitString.strictMajorityOn chooses false on a tie. A Boolean function is symmetric when it depends only on the weight of its input (BooleanFunction.IsSymmetric), and then it factors through the weight (BooleanFunction.IsSymmetric.exists_eq_comp_weight) Jukna, Chapter 1.

Main definitions

• Cslib.BitString.strictMajorityOn: strict majority on a finite set of voting indices.
• Cslib.threshold, Cslib.majority, Cslib.strictMajority: threshold functions.
• Cslib.BooleanFunction.IsSymmetric: Boolean functions depending only on the weight.

Main results

• Cslib.monotone_threshold: threshold functions are monotone.
• Cslib.strictMajority_not: strict majority of the negated bits is the negation of majority.
• Cslib.le_card_ne_of_strictMajority_ne, Cslib.BitString.card_filter_eq_le_half_of_strictMajorityOn_ne: a wrong majority requires at least half wrong votes.
• Cslib.BooleanFunction.IsSymmetric.exists_eq_comp_weight: symmetric functions factor through the weight.
• Cslib.isSymmetric_threshold, Cslib.isSymmetric_majority, Cslib.isSymmetric_strictMajority: threshold functions are symmetric.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.BitString.strictMajorityOn {ι : Type u_1} (s : Finset ι) (vote : ι → Bool) : Bool

Strict majority of the coordinates in s, choosing false on a tie.

theorem Cslib.BitString.card_filter_eq_le_half_of_strictMajorityOn_ne {ι : Type u_1} (s : Finset ι) (vote : ι → Bool) (bit : Bool) (h : strictMajorityOn s vote ≠ bit) : {i ∈ s | vote i = bit}.card ≤ s.card / 2

If strict majority is wrong, at most half of the votes are correct.

@[simp]

theorem Cslib.BitString.strictMajorityOn_const {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (bit : Bool) : (strictMajorityOn s fun (x : ι) => bit) = bit

A nonempty constant vote has its constant value.

def Cslib.threshold (n j : ℕ) : BooleanFunction n

The threshold function Th^n_j on n bits: whether at least j of them are true.

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

The majority function on n bits: whether at least half of them are true, that is, the threshold function Th^n_⌈n/2⌉.

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

The strict majority function on n bits: whether more than half of them are true, so that a tie is false. It is the threshold function Th^n_{⌊n/2⌋+1}.

theorem Cslib.threshold_apply {n : ℕ} (j : ℕ) (x : BitString n) : threshold n j x = decide (j ≤ BitString.weight x)

threshold n j x is the decision of j ≤ weight x.

theorem Cslib.threshold_eq_true_iff {n j : ℕ} {x : BitString n} : threshold n j x = true ↔ j ≤ BitString.weight x

The threshold function Th^n_j is true exactly when at least j bits are true.

theorem Cslib.monotone_threshold {n : ℕ} (j : ℕ) : Monotone (threshold n j)

Threshold functions are monotone.

@[simp]

theorem Cslib.threshold_zero_right {n : ℕ} (x : BitString n) : threshold n 0 x = true

With cutoff 0, the threshold function is the constant true.

theorem Cslib.threshold_eq_false_of_lt {n j : ℕ} (h : n < j) (x : BitString n) : threshold n j x = false

With a cutoff above n, the threshold function is the constant false.

theorem Cslib.threshold_one_right {n : ℕ} (x : BitString n) : threshold n 1 x = decide (∃ (i : Fin n), x i = true)

With cutoff 1, the threshold function is the disjunction.

theorem Cslib.threshold_self {n : ℕ} (x : BitString n) : threshold n n x = decide (∀ (i : Fin n), x i = true)

With cutoff n, the threshold function is the conjunction.

theorem Cslib.majority_eq_true_iff {n : ℕ} {x : BitString n} : majority n x = true ↔ (n + 1) / 2 ≤ BitString.weight x

Majority is true exactly when at least ⌈n/2⌉ = (n + 1) / 2 bits are true.

theorem Cslib.strictMajority_eq_true_iff {n : ℕ} {x : BitString n} : strictMajority n x = true ↔ n / 2 < BitString.weight x

Strict majority is true exactly when more than n / 2 bits are true.

theorem Cslib.strictMajority_eq_false_iff {n : ℕ} {x : BitString n} : strictMajority n x = false ↔ BitString.weight x ≤ n / 2

Strict majority is false exactly when at most n / 2 bits are true.

theorem Cslib.strictMajority_eq_strictMajorityOn {n : ℕ} (x : BitString n) : strictMajority n x = BitString.strictMajorityOn Finset.univ x

Strict majority on all coordinates agrees with the finite-set operation.

theorem Cslib.le_card_ne_of_strictMajority_ne {n : ℕ} {x : BitString n} {y : Bool} (h : strictMajority n x ≠ y) : n - n / 2 ≤ {i : Fin n | x i ≠ y}.card

If the strict majority of n bits is not y, at least n - n / 2 differ from y.

theorem Cslib.strictMajority_not {n : ℕ} (x : BitString n) : (strictMajority n fun (i : Fin n) => !x i) = !majority n x

Strict majority of the negated bits is the negation of majority: fewer than half of the bits are true exactly when not at least half of them are.

def Cslib.BooleanFunction.IsSymmetric {n : ℕ} (f : BooleanFunction n) : Prop

A Boolean function is symmetric when it depends only on the weight of its input.

theorem Cslib.BooleanFunction.IsSymmetric.exists_eq_comp_weight {n : ℕ} {f : BooleanFunction n} (hf : f.IsSymmetric) : ∃ (a : ℕ → Bool), ∀ (x : Fin n → Bool), a (BitString.weight x) = f x

A symmetric function factors through the weight.

theorem Cslib.isSymmetric_threshold {n : ℕ} (j : ℕ) : (threshold n j).IsSymmetric

Threshold functions are symmetric.

theorem Cslib.isSymmetric_majority {n : ℕ} : (majority n).IsSymmetric

Majority is symmetric.

theorem Cslib.isSymmetric_strictMajority {n : ℕ} : (strictMajority n).IsSymmetric

Strict majority is symmetric.