Superquadratic sensitivity separation: agreement with the CSLib measures

The separation construction works with its own measures over an arbitrary finite coordinate type (Internal.sensitivity, Internal.blockSensitivity), defined in terms of BitString.flipOn, 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

• Cslib.BitString.flipOn_eq_flipBlock: on Fin n, BitString.flipOn is BitString.flipBlock.
• 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

@[simp]

theorem Cslib.BitString.flipOn_eq_flipBlock {n : ℕ} {inst : DecidableEq (Fin n)} (T : Finset (Fin n)) (x : BitString n) : flipOn T x = flipBlock T x

On Fin n, BitString.flipOn (with any DecidableEq (Fin n) instance) is CSLib's BitString.flipBlock.

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.