Query complexity measures of threshold functions and parity

The threshold function Th^n_j says that at least j of n bits are true. A coordinate i is sensitive for it at x exactly when x has weight j and x i is true, or (for j ≥ 1) weight j - 1 and x i is false (BitString.isSensitiveCoord_threshold_iff). So the sensitivity is j at an input of weight j and n + 1 - j at an input of weight j - 1. Conversely j true bits certify the value 1 and n + 1 - j false bits certify the value 0 (QueryComplexity.certificateComplexityAt_threshold_le). With s(f) ≤ bs(f) ≤ C(f) all three measures agree: for 1 ≤ j ≤ n, s(Th^n_j) = bs(Th^n_j) = C(Th^n_j) = max(j, n + 1 - j). In particular majority has sensitivity ⌊n/2⌋ + 1 for n ≥ 1. The disjunction OR_n = Th^n_1 is sensitive to every bit at the all-false input, so bs(OR_n) = n. A single true bit certifies its value 1, while certifying the value 0 takes all n bits. Flipping any bit flips the parity, so parity is sensitive to every bit at every input (BitString.sensitivityAt_parity), and its sensitivity, block sensitivity and certificate complexity all equal n. The measures are those of [BdW02].

Main results

• Cslib.BitString.isSensitiveCoord_threshold_iff: the sensitive coordinates of Th^n_j.
• Cslib.BitString.sensitivity_threshold, Cslib.QueryComplexity.blockSensitivity_threshold, Cslib.QueryComplexity.certificateComplexity_threshold: s, bs and C of Th^n_j are max(j, n + 1 - j) for 1 ≤ j ≤ n.
• Cslib.BitString.sensitivity_majority: s(MAJ_n) = ⌊n/2⌋ + 1 for n ≥ 1.
• Cslib.QueryComplexity.blockSensitivity_threshold_one_right: bs(OR_n) = n.
• Cslib.QueryComplexity.certificateComplexity_threshold_one_right: C(OR_n) = n.
• Cslib.QueryComplexity.certificateComplexityFor_threshold_one_right_true, Cslib.QueryComplexity.certificateComplexityFor_threshold_one_right_false: C₁(OR_n) = 1 for n ≥ 1, and C₀(OR_n) = n.
• Cslib.BitString.sensitivity_parity, Cslib.QueryComplexity.blockSensitivity_parity, Cslib.QueryComplexity.certificateComplexity_parity: s, bs and C of parity n are n.

References

• H. Buhrman, R. de Wolf, Complexity measures and decision tree complexity: a survey

theorem Cslib.BitString.isSensitiveCoord_threshold_iff {n j : ℕ} (x : BitString n) (i : Fin n) : IsSensitiveCoord (threshold n j) x i ↔ x i = true ∧ weight x = j ∨ x i = false ∧ weight x + 1 = j

A coordinate is sensitive for Th^n_j exactly when it is a true bit of an input of weight j, or (for j ≥ 1) a false bit of an input of weight j - 1.

theorem Cslib.BitString.sensitivityAt_threshold_of_weight_eq {n j : ℕ} {x : BitString n} (hx : weight x = j) : sensitivityAt (threshold n j) x = j

At an input of weight j, the sensitive coordinates of Th^n_j are its true bits.

theorem Cslib.BitString.sensitivityAt_threshold_of_weight_add_one_eq {n j : ℕ} {x : BitString n} (hx : weight x + 1 = j) : sensitivityAt (threshold n j) x = n + 1 - j

At an input of weight j - 1, for j ≥ 1, the sensitive coordinates of Th^n_j are its false bits.

theorem Cslib.QueryComplexity.certificateComplexityAt_threshold_le {n j : ℕ} (x : BitString n) : certificateComplexityAt (threshold n j) x ≤ max j (n + 1 - j)

Certificate complexity of Th^n_j at any input is at most max(j, n + 1 - j): j true bits certify the value 1, and n + 1 - j false bits certify the value 0.

theorem Cslib.QueryComplexity.blockSensitivity_threshold_le {n j : ℕ} : blockSensitivity (threshold n j) ≤ max j (n + 1 - j)

bs(Th^n_j) ≤ max(j, n + 1 - j).

theorem Cslib.BitString.sensitivity_threshold {n j : ℕ} (hj : 1 ≤ j) (hjn : j ≤ n) : sensitivity (threshold n j) = max j (n + 1 - j)

Sensitivity of threshold functions: s(Th^n_j) = max(j, n + 1 - j) for 1 ≤ j ≤ n.

theorem Cslib.BitString.sensitivity_majority {n : ℕ} (hn : 1 ≤ n) : sensitivity (majority n) = n / 2 + 1

Sensitivity of majority: s(MAJ_n) = ⌊n/2⌋ + 1 for n ≥ 1.

theorem Cslib.QueryComplexity.blockSensitivity_threshold {n j : ℕ} (hj : 1 ≤ j) (hjn : j ≤ n) : blockSensitivity (threshold n j) = max j (n + 1 - j)

Block sensitivity of threshold functions: bs(Th^n_j) = max(j, n + 1 - j) for 1 ≤ j ≤ n.

theorem Cslib.QueryComplexity.certificateComplexity_threshold {n j : ℕ} (hj : 1 ≤ j) (hjn : j ≤ n) : certificateComplexity (threshold n j) = max j (n + 1 - j)

Certificate complexity of threshold functions: C(Th^n_j) = max(j, n + 1 - j) for 1 ≤ j ≤ n.

Disjunction

theorem Cslib.QueryComplexity.sensitivityAt_threshold_one_right {n : ℕ} : (BitString.sensitivityAt (threshold n 1) fun (x : Fin n) => false) = n

The disjunction of n bits is sensitive to every bit at the all-false input.

theorem Cslib.QueryComplexity.blockSensitivity_threshold_one_right {n : ℕ} : blockSensitivity (threshold n 1) = n

The disjunction of n bits has block sensitivity n.

theorem Cslib.QueryComplexity.certificateComplexityAt_threshold_one_right {n : ℕ} : (certificateComplexityAt (threshold n 1) fun (x : Fin n) => false) = n

Certifying the value 0 of the disjunction at the all-false input takes every bit.

theorem Cslib.QueryComplexity.certificateComplexity_threshold_one_right {n : ℕ} : certificateComplexity (threshold n 1) = n

Certificate complexity of disjunction: C(OR_n) = n.

theorem Cslib.QueryComplexity.certificateComplexityFor_threshold_one_right_true {n : ℕ} (hn : 1 ≤ n) : certificateComplexityFor (threshold n 1) true = 1

One true bit certifies the value 1 of the disjunction: C₁(OR_n) = 1 for n ≥ 1.

theorem Cslib.QueryComplexity.certificateComplexityFor_threshold_one_right_false {n : ℕ} : certificateComplexityFor (threshold n 1) false = n

Certifying the value 0 of the disjunction takes every bit: C₀(OR_n) = n.

Parity

theorem Cslib.BitString.sensitivityAt_parity {n : ℕ} (x : BitString n) : sensitivityAt (parity n) x = n

Parity is sensitive to every bit at every input.

theorem Cslib.BitString.sensitivity_parity {n : ℕ} : sensitivity (parity n) = n

The sensitivity of parity is its number of coordinates.

theorem Cslib.QueryComplexity.blockSensitivity_parity {n : ℕ} : blockSensitivity (parity n) = n

The block sensitivity of parity is its number of coordinates.

theorem Cslib.QueryComplexity.certificateComplexity_parity {n : ℕ} : certificateComplexity (parity n) = n

The certificate complexity of parity is its number of coordinates.