Superquadratic sensitivity separation: agreement with the CSLib measures

The separation construction works with its own flips and measures over an arbitrary finite coordinate type (Internal.flip, Internal.sensitivity, Internal.blockSensitivity), since it composes functions on product coordinate types. On the coordinates Fin n these agree with CSLib's BitString.flipBlock, BitString.sensitivity and QueryComplexity.blockSensitivity. Internal block families must consist of nonempty blocks, but this is no restriction: flipping the empty block never changes the value of a function.

Main results

• Internal.flip_eq_flipOn: the internal flip is BitString.flipOn.
• Internal.sensitivity_eq_bitString_sensitivity: the internal sensitivity is BitString.sensitivity.
• Internal.blockSensitivityAt_eq_queryComplexity_blockSensitivityAt, Internal.blockSensitivity_eq_queryComplexity_blockSensitivity: the internal block sensitivity is QueryComplexity.blockSensitivity, pointwise and globally.

References

• N. Nisan, CREW PRAMs and decision trees

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_eq_flipOn {I : Type} [DecidableEq I] (x : I → Bool) (B : Finset I) : flip x B = BitString.flipOn B x

The internal flip is BitString.flipOn, for any decidable equality on the coordinates.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity_eq_bitString_sensitivity {n : ℕ} (f : BooleanFunction n) : sensitivity f = BitString.sensitivity f

On Fin n, the internal sensitivity is BitString.sensitivity.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_eq_queryComplexity_blockSensitivityAt {n : ℕ} (f : BooleanFunction n) (x : BitString n) : blockSensitivityAt f x = QueryComplexity.blockSensitivityAt f x

On Fin n, the internal pointwise block sensitivity is QueryComplexity.blockSensitivityAt.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivity_eq_queryComplexity_blockSensitivity {n : ℕ} (f : BooleanFunction n) : blockSensitivity f = QueryComplexity.blockSensitivity f

On Fin n, the internal block sensitivity is QueryComplexity.blockSensitivity.