Boolean function complexity measures

Sensitivity s(f), block sensitivity bs(f) and certificate complexity C(f), together with the chain s(f) ≤ bs(f) ≤ C(f). Notation follows [AB09]; the pointwise measures s(f, x), bs(f, x), C(f, x) are those of Jukna, Section 14.3.

Main definitions

• BitString.sensitivity: s(f), the maximum over inputs of the number of sensitive coordinates.
• blockSensitivity: bs(f), the maximum over inputs of the maximum number of disjoint sensitive blocks.
• IsCertificate: a set of coordinates whose values at x pin down f x, as in Jukna, Section 14.3.
• Forces: a partial assignment forces the value b, as in [BdW02]. At a fixed input an assignment consistent with x is determined by its support, so the pointwise measure needs no bit values.
• certificateComplexity: C(f), the maximum over inputs of the smallest certificate size.

Main results

• sensitivity_le_blockSensitivity: s(f) ≤ bs(f).
• blockSensitivity_le_certificateComplexity: bs(f) ≤ C(f).
• isCertificate_iff_forces_restrict, forces_iff_isCertificate_support: IsCertificate and Forces agree at a fixed input.
• certificateComplexityAt_eq_inf'_size: C(f, x) is the minimum size of a forcing assignment consistent with x.
• |B| ≤ s(f) for a minimal sensitive block B.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 12.2 (Certificate Complexity) and Section 12.5.1 (Sensitivity).
• H. Buhrman, R. de Wolf, Complexity measures and decision tree complexity: a survey
• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Section 14.3.

Sensitivity

def Cslib.BitString.IsSensitiveCoord {n : ℕ} (f : BooleanFunction n) (x : BitString n) (i : Fin n) : Prop

Coordinate i is sensitive for f at x when flipping it flips f.

Equations

• Cslib.BitString.IsSensitiveCoord f x i = (f (Function.update x i !x i) ≠ f x)

@[instance_reducible]

instance Cslib.BitString.instDecidablePredFinIsSensitiveCoord {n : ℕ} (f : BooleanFunction n) (x : BitString n) : DecidablePred (IsSensitiveCoord f x)

Equations

• Cslib.BitString.instDecidablePredFinIsSensitiveCoord f x i = { decide := !decide (f (Function.update x i !x i) = f x), reflects_decide := ⋯ }

def Cslib.BitString.sensitiveCoords {n : ℕ} (f : BooleanFunction n) (x : BitString n) : Finset (Fin n)

The set of coordinates sensitive for f at x.

Equations

• Cslib.BitString.sensitiveCoords f x = Finset.filter (Cslib.BitString.IsSensitiveCoord f x) Finset.univ

@[simp]

theorem Cslib.BitString.mem_sensitiveCoords {n : ℕ} {f : BooleanFunction n} {x : BitString n} {i : Fin n} : i ∈ sensitiveCoords f x ↔ IsSensitiveCoord f x i

The bridge between the predicate and the Finset it cuts out.

def Cslib.BitString.sensitivityAt {n : ℕ} (f : BooleanFunction n) (x : BitString n) : ℕ

The number of sensitive coordinates in input x, usually denoted s(f, x).

Equations

• Cslib.BitString.sensitivityAt f x = (Cslib.BitString.sensitiveCoords f x).card

def Cslib.BitString.sensitivity {n : ℕ} (f : BooleanFunction n) : ℕ

The maximum sensitivity over all inputs, denoted s(f).

Equations

• Cslib.BitString.sensitivity f = Finset.univ.sup (Cslib.BitString.sensitivityAt f)

theorem Cslib.BitString.card_le_sensitivityAt {n : ℕ} {f : BooleanFunction n} {x : BitString n} {S : Finset (Fin n)} (h : ∀ i ∈ S, IsSensitiveCoord f x i) : S.card ≤ sensitivityAt f x

Lower-bound rule for s(f, x): exhibit a set of sensitive coordinates.

theorem Cslib.BitString.sensitivityAt_le_sensitivity {n : ℕ} (f : BooleanFunction n) (x : BitString n) : sensitivityAt f x ≤ sensitivity f

The sensitivity at a single input is at most the sensitivity of f: s(f, x) ≤ s(f).

theorem Cslib.BitString.card_le_sensitivity_of_forall_isSensitiveCoord {n : ℕ} {f : BooleanFunction n} {x : BitString n} {S : Finset (Fin n)} (h : ∀ i ∈ S, IsSensitiveCoord f x i) : S.card ≤ sensitivity f

Lower-bound rule for s(f): sensitive coordinates at any input suffice.

theorem Cslib.BitString.sensitivityAt_le_card {n : ℕ} (f : BooleanFunction n) (x : BitString n) : sensitivityAt f x ≤ n

s(f, x) ≤ n: there are only n coordinates.

theorem Cslib.BitString.sensitivity_le_card {n : ℕ} (f : BooleanFunction n) : sensitivity f ≤ n

s(f) ≤ n.

Block sensitivity

def Cslib.QueryComplexity.IsSensitiveBlock {n : ℕ} (f : BooleanFunction n) (x : BitString n) (B : Block n) : Prop

Block B is sensitive for f at x when flipping all bits of B flips f.

Equations

• Cslib.QueryComplexity.IsSensitiveBlock f x B = (f (Cslib.BitString.flipBlock B x) ≠ f x)

@[instance_reducible]

instance Cslib.QueryComplexity.instDecidableIsSensitiveBlock {n : ℕ} (f : BooleanFunction n) (x : BitString n) (B : Block n) : Decidable (IsSensitiveBlock f x B)

Equations

• Cslib.QueryComplexity.instDecidableIsSensitiveBlock f x B = { decide := !decide (f (Cslib.BitString.flipBlock B x) = f x), reflects_decide := ⋯ }

def Cslib.QueryComplexity.IsSensitiveFamily {n : ℕ} (f : BooleanFunction n) (x : BitString n) (F : Finset (Block n)) : Prop

Every member flips f, and the members are pairwise disjoint.

Equations

• Cslib.QueryComplexity.IsSensitiveFamily f x F = ((∀ B ∈ F, Cslib.QueryComplexity.IsSensitiveBlock f x B) ∧ (↑F).PairwiseDisjoint id)

@[instance_reducible]

instance Cslib.QueryComplexity.instDecidableIsSensitiveFamily {n : ℕ} (f : BooleanFunction n) (x : BitString n) (F : Finset (Block n)) : Decidable (IsSensitiveFamily f x F)

Equations

• Cslib.QueryComplexity.instDecidableIsSensitiveFamily f x F = decidable_of_iff ((∀ B ∈ F, Cslib.QueryComplexity.IsSensitiveBlock f x B) ∧ ∀ P ∈ F, ∀ Q ∈ F, P ≠ Q → Disjoint P Q) ⋯

def Cslib.QueryComplexity.sensitiveFamilies {n : ℕ} (f : BooleanFunction n) (x : BitString n) : Finset (Finset (Block n))

All sensitive families.

Equations

• Cslib.QueryComplexity.sensitiveFamilies f x = Finset.filter (Cslib.QueryComplexity.IsSensitiveFamily f x) Finset.univ

@[simp]

theorem Cslib.QueryComplexity.mem_sensitiveFamilies {n : ℕ} {f : BooleanFunction n} {x : BitString n} {F : Finset (Block n)} : F ∈ sensitiveFamilies f x ↔ IsSensitiveFamily f x F

def Cslib.QueryComplexity.blockSensitivityAt {n : ℕ} (f : BooleanFunction n) (x : BitString n) : ℕ

The block sensitivity of f at x: the largest number of pairwise disjoint blocks of coordinates such that flipping every coordinate of any one block flips f. Usually denoted bs(f, x).

Equations

• Cslib.QueryComplexity.blockSensitivityAt f x = (Cslib.QueryComplexity.sensitiveFamilies f x).sup Finset.card

def Cslib.QueryComplexity.blockSensitivity {n : ℕ} (f : BooleanFunction n) : ℕ

The maximum block sensitivity over all inputs, denoted bs(f).

Equations

• Cslib.QueryComplexity.blockSensitivity f = Finset.univ.sup (Cslib.QueryComplexity.blockSensitivityAt f)

theorem Cslib.QueryComplexity.card_le_blockSensitivityAt {n : ℕ} {f : BooleanFunction n} {x : BitString n} {F : Finset (Block n)} (h : IsSensitiveFamily f x F) : F.card ≤ blockSensitivityAt f x

Lower-bound rule for bs(f, x): exhibit one sensitive family.

theorem Cslib.QueryComplexity.blockSensitivityAt_le_blockSensitivity {n : ℕ} (f : BooleanFunction n) (x : BitString n) : blockSensitivityAt f x ≤ blockSensitivity f

The block sensitivity at a single input is at most that of f: bs(f, x) ≤ bs(f).

theorem Cslib.QueryComplexity.card_le_blockSensitivity {n : ℕ} {f : BooleanFunction n} {x : BitString n} {F : Finset (Block n)} (h : IsSensitiveFamily f x F) : F.card ≤ blockSensitivity f

Lower-bound rule for bs(f).

Sensitive singletons

@[simp]

theorem Cslib.QueryComplexity.isSensitiveBlock_singleton {n : ℕ} {f : BooleanFunction n} {x : BitString n} {i : Fin n} : IsSensitiveBlock f x {i} ↔ BitString.IsSensitiveCoord f x i

A singleton block is sensitive if and only if its coordinate is.

s(f) ≤ bs(f)

def Cslib.QueryComplexity.singletonFamily {n : ℕ} (f : BooleanFunction n) (x : BitString n) : Finset (Block n)

One block per sensitive coordinate.

Equations

• Cslib.QueryComplexity.singletonFamily f x = Finset.image (fun (i : Fin n) => {i}) (Cslib.BitString.sensitiveCoords f x)

@[simp]

theorem Cslib.QueryComplexity.mem_singletonFamily {n : ℕ} {f : BooleanFunction n} {x : BitString n} {B : Block n} : B ∈ singletonFamily f x ↔ ∃ (i : Fin n), BitString.IsSensitiveCoord f x i ∧ {i} = B

Membership in the singleton family: one block per sensitive coordinate.

@[simp]

theorem Cslib.QueryComplexity.card_singletonFamily {n : ℕ} {f : BooleanFunction n} {x : BitString n} : (singletonFamily f x).card = BitString.sensitivityAt f x

The singleton family has one block per sensitive coordinate, so s(f, x) of them.

theorem Cslib.QueryComplexity.isSensitiveFamily_singletonFamily {n : ℕ} {f : BooleanFunction n} {x : BitString n} : IsSensitiveFamily f x (singletonFamily f x)

Singletons of distinct sensitive coordinates do form a sensitive family: each flips f, and distinct singletons are disjoint.

theorem Cslib.QueryComplexity.sensitivityAt_le_blockSensitivityAt {n : ℕ} (f : BooleanFunction n) (x : BitString n) : BitString.sensitivityAt f x ≤ blockSensitivityAt f x

Pointwise: s(f, x) ≤ bs(f, x).

theorem Cslib.QueryComplexity.sensitivity_le_blockSensitivity {n : ℕ} (f : BooleanFunction n) : BitString.sensitivity f ≤ blockSensitivity f

Every sensitive coordinate is a sensitive block of size one, so s(f) ≤ bs(f).

Minimal sensitive blocks

def Cslib.QueryComplexity.IsMinimalSensitiveBlock {n : ℕ} (f : BooleanFunction n) (x : BitString n) (B : Block n) : Prop

B is sensitive, and no proper subset of B is sensitive.

Equations

• Cslib.QueryComplexity.IsMinimalSensitiveBlock f x B = (Cslib.QueryComplexity.IsSensitiveBlock f x B ∧ ∀ C ⊂ B, ¬Cslib.QueryComplexity.IsSensitiveBlock f x C)

@[instance_reducible]

instance Cslib.QueryComplexity.instDecidableIsMinimalSensitiveBlock {n : ℕ} (f : BooleanFunction n) (x : BitString n) (B : Block n) : Decidable (IsMinimalSensitiveBlock f x B)

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.QueryComplexity.IsMinimalSensitiveBlock.not_isSensitiveBlock_erase {n : ℕ} {f : BooleanFunction n} {x : BitString n} {B : Block n} {i : Fin n} (hB : IsMinimalSensitiveBlock f x B) (hi : i ∈ B) : ¬IsSensitiveBlock f x (Finset.erase B i)

Dropping any coordinate from a minimal sensitive block breaks sensitivity.

theorem Cslib.QueryComplexity.IsMinimalSensitiveBlock.isSensitiveCoord_flipBlock {n : ℕ} {f : BooleanFunction n} {x : BitString n} {B : Block n} {i : Fin n} (hB : IsMinimalSensitiveBlock f x B) (hi : i ∈ B) : BitString.IsSensitiveCoord f (BitString.flipBlock B x) i

Every coordinate of a minimal sensitive block is sensitive at the input which has the minimal sensitive block flipped.

theorem Cslib.QueryComplexity.IsMinimalSensitiveBlock.card_le_sensitivity {n : ℕ} {f : BooleanFunction n} {x : BitString n} {B : Block n} (hB : IsMinimalSensitiveBlock f x B) : Finset.card B ≤ BitString.sensitivity f

|B| ≤ s(f) for a minimal sensitive block B.

Certificates

A certificate for x is a set of coordinates whose values at x already determine f x Jukna, Section 14.3. The survey [BdW02] instead works with partial assignments that force a value; Forces keeps that in general form, with the forced value b a parameter, and the two views agree at a fixed input.

def Cslib.QueryComplexity.IsCertificate {n : ℕ} (f : BooleanFunction n) (x : BitString n) (S : Finset (Fin n)) : Prop

S is a certificate for f at x: every input agreeing with x on S takes the same value, so f x can be read off from the bits of x in S.

Equations

• Cslib.QueryComplexity.IsCertificate f x S = ∀ (y : Cslib.BitString n), (∀ i ∈ S, y i = x i) → f y = f x

@[instance_reducible]

instance Cslib.QueryComplexity.instDecidableIsCertificate {n : ℕ} (f : BooleanFunction n) (x : BitString n) (S : Finset (Fin n)) : Decidable (IsCertificate f x S)

Equations

• Cslib.QueryComplexity.instDecidableIsCertificate f x S = { decide := decide (∀ a ∈ Finset.univ, (fun (y : Cslib.BitString n) => (∀ i ∈ S, y i = x i) → f y = f x) a), reflects_decide := ⋯ }

def Cslib.QueryComplexity.Forces {n : ℕ} (f : BooleanFunction n) (C : PartialAssignment n) (b : Bool) : Prop

C forces the value b: everything consistent with C has f = b.

Equations

• Cslib.QueryComplexity.Forces f C b = ∀ (x : Cslib.BitString n), Cslib.QueryComplexity.Agrees C x → f x = b

@[instance_reducible]

instance Cslib.QueryComplexity.instDecidableForces {n : ℕ} (f : BooleanFunction n) (C : PartialAssignment n) (b : Bool) : Decidable (Forces f C b)

Equations

• Cslib.QueryComplexity.instDecidableForces f C b = { decide := decide (∀ a ∈ Finset.univ, (fun (x : Cslib.BitString n) => Cslib.QueryComplexity.Agrees C x → f x = b) a), reflects_decide := ⋯ }

theorem Cslib.QueryComplexity.isCertificate_iff_forces_restrict {n : ℕ} {f : BooleanFunction n} {x : BitString n} {S : Finset (Fin n)} : IsCertificate f x S ↔ Forces f (restrict x S) (f x)

S is a certificate for x if and only if x restricted to S forces f x.

theorem Cslib.QueryComplexity.forces_iff_isCertificate_support {n : ℕ} {f : BooleanFunction n} {x : BitString n} {C : PartialAssignment n} (hC : Agrees C x) : Forces f C (f x) ↔ IsCertificate f x (support C)

A partial assignment consistent with x forces f x if and only if its support is a certificate for x.

theorem Cslib.QueryComplexity.isCertificate_univ {n : ℕ} (f : BooleanFunction n) (x : BitString n) : IsCertificate f x Finset.univ

Reading every coordinate of x is a certificate.

theorem Cslib.QueryComplexity.filter_isCertificate_nonempty {n : ℕ} (f : BooleanFunction n) (x : BitString n) : (Finset.filter (IsCertificate f x) Finset.univ).Nonempty

There is always a certificate, so C(f, x) is a minimum over a non-empty set.

def Cslib.QueryComplexity.certificateComplexityAt {n : ℕ} (f : BooleanFunction n) (x : BitString n) : ℕ

The fewest coordinates of x that pin down the value of f, denoted C(f, x).

Equations

• Cslib.QueryComplexity.certificateComplexityAt f x = (Finset.filter (Cslib.QueryComplexity.IsCertificate f x) Finset.univ).inf' ⋯ Finset.card

theorem Cslib.QueryComplexity.certificateComplexityAt_le {n : ℕ} {f : BooleanFunction n} {x : BitString n} {S : Finset (Fin n)} (h : IsCertificate f x S) : certificateComplexityAt f x ≤ S.card

Upper-bound rule for C(f, x): exhibit one certificate.

theorem Cslib.QueryComplexity.le_certificateComplexityAt {n : ℕ} {f : BooleanFunction n} {x : BitString n} {k : ℕ} (h : ∀ (S : Finset (Fin n)), IsCertificate f x S → k ≤ S.card) : k ≤ certificateComplexityAt f x

Lower-bound rule for C(f, x): a bound that holds for every certificate.

theorem Cslib.QueryComplexity.exists_isCertificate_card_eq {n : ℕ} (f : BooleanFunction n) (x : BitString n) : ∃ (S : Finset (Fin n)), IsCertificate f x S ∧ S.card = certificateComplexityAt f x

Some certificate for x has exactly C(f, x) coordinates.

Certificates as partial assignments

At a fixed input a forcing assignment carries no information beyond the coordinates it reads: Agrees C x forces C i = some (x i) on the support and none elsewhere. So C(f, x) over coordinate sets is also the minimum size of a forcing assignment consistent with x.

def Cslib.QueryComplexity.forcingAssignments {n : ℕ} (f : BooleanFunction n) (x : BitString n) : Finset (PartialAssignment n)

Partial assignments consistent with x that force f x.

Equations

• Cslib.QueryComplexity.forcingAssignments f x = {C : Cslib.QueryComplexity.PartialAssignment n | Cslib.QueryComplexity.Agrees C x ∧ Cslib.QueryComplexity.Forces f C (f x)}

@[simp]

theorem Cslib.QueryComplexity.mem_forcingAssignments {n : ℕ} {f : BooleanFunction n} {x : BitString n} {C : PartialAssignment n} : C ∈ forcingAssignments f x ↔ Agrees C x ∧ Forces f C (f x)

theorem Cslib.QueryComplexity.ofBitString_mem_forcingAssignments {n : ℕ} (f : BooleanFunction n) (x : BitString n) : ofBitString x ∈ forcingAssignments f x

Reading off all of x forces f x.

theorem Cslib.QueryComplexity.forcingAssignments_nonempty {n : ℕ} (f : BooleanFunction n) (x : BitString n) : (forcingAssignments f x).Nonempty

There is always a forcing assignment consistent with x.

theorem Cslib.QueryComplexity.certificateComplexityAt_eq_inf'_size {n : ℕ} (f : BooleanFunction n) (x : BitString n) : certificateComplexityAt f x = (forcingAssignments f x).inf' ⋯ size

C(f, x) over coordinate sets is the minimum size of a forcing assignment consistent with x, the definition of [BdW02].

def Cslib.QueryComplexity.certificateComplexity {n : ℕ} (f : BooleanFunction n) : ℕ

The maximum over all inputs of the smallest certificate size, denoted C(f).

Equations

• Cslib.QueryComplexity.certificateComplexity f = Finset.univ.sup (Cslib.QueryComplexity.certificateComplexityAt f)

theorem Cslib.QueryComplexity.certificateComplexityAt_le_certificateComplexity {n : ℕ} (f : BooleanFunction n) (x : BitString n) : certificateComplexityAt f x ≤ certificateComplexity f

The certificate complexity at a single input is at most that of f: C(f, x) ≤ C(f).

theorem Cslib.QueryComplexity.certificateComplexityAt_le_card {n : ℕ} (f : BooleanFunction n) (x : BitString n) : certificateComplexityAt f x ≤ n

C(f, x) ≤ n: reading every coordinate pins down f.

theorem Cslib.QueryComplexity.certificateComplexity_le_card {n : ℕ} (f : BooleanFunction n) : certificateComplexity f ≤ n

C(f) ≤ n.

bs(f) ≤ C(f)

A certificate for x must meet every block of a sensitive family. The blocks are pairwise disjoint, so a family has at most |S| members.

theorem Cslib.QueryComplexity.sensitiveBlock_inter_nonempty {n : ℕ} {f : BooleanFunction n} {x : BitString n} {B : Block n} (hB : IsSensitiveBlock f x B) {S : Finset (Fin n)} (hS : IsCertificate f x S) : Finset.Nonempty (B ∩ S)

A certificate must contain at least one coordinate of every sensitive block.

theorem Cslib.QueryComplexity.card_le_card_of_isSensitiveFamily {n : ℕ} {f : BooleanFunction n} {x : BitString n} {F : Finset (Block n)} {S : Finset (Fin n)} (hF : IsSensitiveFamily f x F) (hS : IsCertificate f x S) : F.card ≤ S.card

A certificate is at least as large as any sensitive family.

theorem Cslib.QueryComplexity.blockSensitivityAt_le_certificateComplexityAt {n : ℕ} (f : BooleanFunction n) (x : BitString n) : blockSensitivityAt f x ≤ certificateComplexityAt f x

Pointwise: bs(f, x) ≤ C(f, x).

theorem Cslib.QueryComplexity.blockSensitivity_le_certificateComplexity {n : ℕ} (f : BooleanFunction n) : blockSensitivity f ≤ certificateComplexity f

Every block of a sensitive family meets every certificate, so bs(f) ≤ C(f).

theorem Cslib.QueryComplexity.blockSensitivityAt_le_card {n : ℕ} (f : BooleanFunction n) (x : BitString n) : blockSensitivityAt f x ≤ n

bs(f, x) ≤ n.

theorem Cslib.QueryComplexity.blockSensitivity_le_card {n : ℕ} (f : BooleanFunction n) : blockSensitivity f ≤ n

bs(f) ≤ n.