Superquadratic sensitivity separation: composition

Disjoint Boolean composition compose f g on the coordinate type I × J: the inner function g is evaluated on each row fun j => x (i, j), and the outer function f on the resulting vector of row values, so each child keeps its own raw coordinates. Sensitivity is submultiplicative under composition, while block sensitivity at the all-false input is supermultiplicative when g rejects the all-false input.

Main definitions

• compose: block composition x ↦ f (fun i => g (fun j => x (i, j))).

Main results

• compose_flip_sensitive_iff: coordinate (i, j) is sensitive for compose f g iff j is sensitive for g on row i and i is sensitive for f on the row values.
• sensitivityAt_compose: the sensitivity of compose f g at x is the sum of the inner sensitivities over the rows that are sensitive for f.
• sensitivity_compose_le: sensitivity (compose f g) ≤ sensitivity f * sensitivity g.
• blockSensitivityAt_compose_zero_le: block sensitivities at the all-false input are supermultiplicative under composition, provided g rejects the all-false input.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/Composition.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.compose {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) : (I × J → Bool) → Bool

Block composition: evaluate the inner function in each row, then the outer function.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.compose_flip_sensitive_iff {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (x : I × J → Bool) (i : I) (j : J) : compose f g (flip x {(i, j)}) ≠ compose f g x ↔ (g (flip (fun (a : J) => x (i, a)) {j}) ≠ g fun (a : J) => x (i, a)) ∧ f (flip (fun (k : I) => g fun (a : J) => x (k, a)) {i}) ≠ f fun (k : I) => g fun (a : J) => x (k, a)

Flipping coordinate (i, j) changes compose f g x iff flipping j changes the value of g on row i of x, and flipping i changes the value of f on the vector of row values fun k => g (fun a => x (k, a)).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.compose_zero {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (hg : (g fun (x : J) => false) = false) : (compose f g fun (x : I × J) => false) = f fun (x : I) => false

If g rejects the all-false input, then compose f g and f take the same value on the all-false input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivityAt_compose {I J : Type} [Fintype I] [Fintype J] (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (x : I × J → Bool) : sensitivityAt (compose f g) x = ∑ i : I with f (flip (fun (k : I) => g fun (a : J) => x (k, a)) {i}) ≠ f fun (k : I) => g fun (a : J) => x (k, a), sensitivityAt g fun (a : J) => x (i, a)

The sensitivity of compose f g at x equals the sum, over the rows i that are sensitive for f at the vector of row values, of the sensitivity of g at row i of x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity_compose_le {I J : Type} [Fintype I] [Fintype J] (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) : sensitivity (compose f g) ≤ sensitivity f * sensitivity g

Sensitivity is submultiplicative under composition: sensitivity (compose f g) ≤ sensitivity f * sensitivity g.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_compose_zero_le {I J : Type} [Fintype I] [Fintype J] (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (hg : (g fun (x : J) => false) = false) : ((blockSensitivityAt f fun (x : I) => false) * blockSensitivityAt g fun (x : J) => false) ≤ blockSensitivityAt (compose f g) fun (x : I × J) => false

If g rejects the all-false input, then the product of the block sensitivities of f and g at the all-false input is at most the block sensitivity of compose f g there.