Query complexity of monotone functions

For a monotone Boolean function, certificate complexity, block sensitivity and sensitivity coincide: C(f) = bs(f) = s(f) [Nis91]. Let f(x) = 1 and let y ≤ x be an input of value 1 of least weight below x. Clearing any true bit of y gives a lighter input below x, which has value 0, so every true bit of y is sensitive at y. Conversely every input agreeing with x on the true bits of y lies above y, so has value 1. So the true bits of y certify x, and C(f, x) ≤ s(f, y) ≤ s₁(f). Dually C(f, x) ≤ s₀(f) when f(x) = 0, using an input of value 0 of largest weight above x. With D(f) ≤ C₀(f) C₁(f) this gives D(f) ≤ s₀(f) s₁(f) ≤ s(f)² for monotone f.

Main results

• Cslib.QueryComplexity.certificateComplexityFor_le_sensitivityFor_of_monotone: C_b(f) ≤ s_b(f) for monotone f.
• Cslib.QueryComplexity.certificateComplexity_eq_sensitivity_of_monotone, Cslib.QueryComplexity.blockSensitivity_eq_sensitivity_of_monotone: C(f) = s(f) and bs(f) = s(f) for monotone f.
• Cslib.DecisionTree.complexity_le_sensitivityFor_mul_sensitivityFor_of_monotone, Cslib.DecisionTree.complexity_le_sensitivity_sq_of_monotone: D(f) ≤ s₀(f) s₁(f) ≤ s(f)² for monotone f.

References

• N. Nisan, CREW PRAMs and decision trees
• H. Buhrman, R. de Wolf, Complexity measures and decision tree complexity: a survey

theorem Cslib.QueryComplexity.certificateComplexityAt_le_sensitivityFor_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) (x : BitString n) : certificateComplexityAt f x ≤ BitString.sensitivityFor f (f x)

For a monotone function, C(f, x) ≤ s_{f(x)}(f).

theorem Cslib.QueryComplexity.certificateComplexityFor_le_sensitivityFor_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) (b : Bool) : certificateComplexityFor f b ≤ BitString.sensitivityFor f b

For a monotone function, C_b(f) ≤ s_b(f).

theorem Cslib.QueryComplexity.certificateComplexity_eq_sensitivity_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) : certificateComplexity f = BitString.sensitivity f

Certificate complexity of monotone functions [Nis91]: C(f) = s(f).

theorem Cslib.QueryComplexity.blockSensitivity_eq_sensitivity_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) : blockSensitivity f = BitString.sensitivity f

Block sensitivity of monotone functions [Nis91]: bs(f) = s(f).

theorem Cslib.DecisionTree.complexity_le_sensitivityFor_mul_sensitivityFor_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) : complexity f ≤ BitString.sensitivityFor f false * BitString.sensitivityFor f true

For a monotone function, D(f) ≤ s₀(f) s₁(f).

theorem Cslib.DecisionTree.complexity_le_sensitivity_sq_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) : complexity f ≤ BitString.sensitivity f ^ 2

For a monotone function, D(f) ≤ s(f)².