Superquadratic sensitivity separation: model

This file fixes the model of Boolean functions f : (I → Bool) → Bool used throughout the separation: flipping a finite set of input coordinates, the sensitivity of f at an input and overall, and the block sensitivity of f at an input and overall. All maxima are Finset.sups over the actual finite input space or the finite space of block families, so the definitions agree literally with the standard ones. These measures are internal to the construction, which needs arbitrary finite coordinate types; Bridge identifies them on Fin n with CSLib's BitString.sensitivity and QueryComplexity.blockSensitivity.

Main definitions

• flip: negate the coordinates of an input lying in a given finite set; this is BitString.flipOn with the arguments swapped and classical decidable equality.
• sensitivityAt: the number of coordinates whose flip changes f x.
• sensitivity: the maximum of sensitivityAt f x over all inputs x.
• blockSensitivityAt: the maximum number of disjoint nonempty blocks whose flips change f x.
• blockSensitivity: the maximum of blockSensitivityAt f x over all inputs x.

References

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

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.flip {I : Type} (x : I → Bool) (B : Finset I) : I → Bool

Flip exactly the coordinates belonging to the specified block.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_apply {I : Type} (x : I → Bool) (B : Finset I) (i : I) : flip x B i = if i ∈ B then !x i else x i

Coordinatewise, flip x B negates exactly the coordinates in B.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : ℕ

The ordinary number of sensitive individual input coordinates.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) : ℕ

Maximum ordinary sensitivity over all Boolean inputs.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : ℕ

Maximum size of a family of disjoint nonempty sensitive blocks at an input. The empty family is allowed and contributes zero. Invalid families contribute zero.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) : ℕ

Maximum block sensitivity over all Boolean inputs.