One-sided query complexity measures and negation

For a value b, the one-sided measures s_b(f), bs_b(f) and C_b(f) are the largest sensitivity, block sensitivity and certificate complexity of f at an input of value b (BitString.sensitivityFor, QueryComplexity.blockSensitivityFor, QueryComplexity.certificateComplexityFor) [BdW02].

Negation keeps sensitive coordinates, sensitive blocks and certificates, so it preserves s, bs and C and exchanges the two values of the one-sided measures (BitString.sensitivityFor_not, QueryComplexity.blockSensitivityFor_not, QueryComplexity.certificateComplexityFor_not).

Main definitions

• Cslib.BitString.sensitivityFor: the sensitivity s_b(f) of the inputs where f has value b.
• Cslib.QueryComplexity.blockSensitivityFor: the block sensitivity bs_b(f) of the inputs where f has value b.
• Cslib.QueryComplexity.certificateComplexityFor: the certificate complexity C_b(f) of the inputs where f has value b.

Main results

• Cslib.BitString.sensitivity_not, Cslib.QueryComplexity.blockSensitivity_not, Cslib.QueryComplexity.certificateComplexity_not: negation preserves s, bs and C.
• Cslib.BitString.sensitivityFor_not, Cslib.QueryComplexity.blockSensitivityFor_not, Cslib.QueryComplexity.certificateComplexityFor_not: negation exchanges the two values of the one-sided measures.

References

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

def Cslib.BitString.sensitivityFor {n : ℕ} (f : BooleanFunction n) (b : Bool) : ℕ

s_b(f): the largest sensitivity of f at an input where it has value b.

theorem Cslib.BitString.sensitivityAt_le_sensitivityFor {n : ℕ} {f : BooleanFunction n} {x : BitString n} {b : Bool} (h : f x = b) : sensitivityAt f x ≤ sensitivityFor f b

The sensitivity at an input of value b is at most s_b(f).

theorem Cslib.BitString.sensitivityFor_le_sensitivity {n : ℕ} (f : BooleanFunction n) (b : Bool) : sensitivityFor f b ≤ sensitivity f

s_b(f) ≤ s(f).

@[simp]

theorem Cslib.BitString.isSensitiveCoord_not {n : ℕ} {f : BooleanFunction n} {x : BitString n} {i : Fin n} : IsSensitiveCoord (fun (y : BitString n) => !f y) x i ↔ IsSensitiveCoord f x i

Negating a function keeps its sensitive coordinates.

theorem Cslib.BitString.sensitivityAt_not {n : ℕ} (f : BooleanFunction n) (x : BitString n) : sensitivityAt (fun (y : BitString n) => !f y) x = sensitivityAt f x

Negation preserves the sensitivity at an input.

theorem Cslib.BitString.sensitivity_not {n : ℕ} (f : BooleanFunction n) : (sensitivity fun (y : BitString n) => !f y) = sensitivity f

Negation preserves sensitivity.

theorem Cslib.BitString.sensitivityFor_not {n : ℕ} (f : BooleanFunction n) (b : Bool) : sensitivityFor (fun (y : BitString n) => !f y) b = sensitivityFor f !b

Negation exchanges s₀ and s₁.

def Cslib.QueryComplexity.blockSensitivityFor {n : ℕ} (f : BooleanFunction n) (b : Bool) : ℕ

bs_b(f): the largest block sensitivity of f at an input where it has value b.

theorem Cslib.QueryComplexity.blockSensitivityAt_le_blockSensitivityFor {n : ℕ} {f : BooleanFunction n} {x : BitString n} {b : Bool} (h : f x = b) : blockSensitivityAt f x ≤ blockSensitivityFor f b

The block sensitivity at an input of value b is at most bs_b(f).

theorem Cslib.QueryComplexity.blockSensitivityFor_le_blockSensitivity {n : ℕ} (f : BooleanFunction n) (b : Bool) : blockSensitivityFor f b ≤ blockSensitivity f

bs_b(f) ≤ bs(f).

def Cslib.QueryComplexity.certificateComplexityFor {n : ℕ} (f : BooleanFunction n) (b : Bool) : ℕ

C_b(f): the largest certificate complexity of f at an input where it has value b.

theorem Cslib.QueryComplexity.certificateComplexityAt_le_certificateComplexityFor {n : ℕ} {f : BooleanFunction n} {x : BitString n} {b : Bool} (h : f x = b) : certificateComplexityAt f x ≤ certificateComplexityFor f b

The certificate complexity at an input of value b is at most C_b(f).

theorem Cslib.QueryComplexity.certificateComplexityFor_le_certificateComplexity {n : ℕ} (f : BooleanFunction n) (b : Bool) : certificateComplexityFor f b ≤ certificateComplexity f

C_b(f) ≤ C(f).

@[simp]

theorem Cslib.QueryComplexity.isSensitiveBlock_not {n : ℕ} {f : BooleanFunction n} {x : BitString n} {B : Block n} : IsSensitiveBlock (fun (y : BitString n) => !f y) x B ↔ IsSensitiveBlock f x B

Negating a function keeps its sensitive blocks.

@[simp]

theorem Cslib.QueryComplexity.isCertificate_not {n : ℕ} {f : BooleanFunction n} {x : BitString n} {S : Finset (Fin n)} : IsCertificate (fun (y : BitString n) => !f y) x S ↔ IsCertificate f x S

Negating a function keeps its certificates.

theorem Cslib.QueryComplexity.blockSensitivityAt_not {n : ℕ} (f : BooleanFunction n) (x : BitString n) : blockSensitivityAt (fun (y : BitString n) => !f y) x = blockSensitivityAt f x

Negation preserves the block sensitivity at an input.

theorem Cslib.QueryComplexity.certificateComplexityAt_not {n : ℕ} (f : BooleanFunction n) (x : BitString n) : certificateComplexityAt (fun (y : BitString n) => !f y) x = certificateComplexityAt f x

Negation preserves the certificate complexity at an input.

theorem Cslib.QueryComplexity.blockSensitivity_not {n : ℕ} (f : BooleanFunction n) : (blockSensitivity fun (y : BitString n) => !f y) = blockSensitivity f

Negation preserves block sensitivity.

theorem Cslib.QueryComplexity.certificateComplexity_not {n : ℕ} (f : BooleanFunction n) : (certificateComplexity fun (y : BitString n) => !f y) = certificateComplexity f

Negation preserves certificate complexity.

theorem Cslib.QueryComplexity.blockSensitivityFor_not {n : ℕ} (f : BooleanFunction n) (b : Bool) : blockSensitivityFor (fun (y : BitString n) => !f y) b = blockSensitivityFor f !b

Negation exchanges bs₀ and bs₁.

theorem Cslib.QueryComplexity.certificateComplexityFor_not {n : ℕ} (f : BooleanFunction n) (b : Bool) : certificateComplexityFor (fun (y : BitString n) => !f y) b = certificateComplexityFor f !b

Negation exchanges C₀ and C₁.