Superquadratic sensitivity separation: reindex

Transport reindex e f of a Boolean function f along an equivalence e : I ≃ J of coordinate types. Global sensitivity and pointwise block sensitivity are invariant under reindexing, which allows functions on structured coordinate types to be moved onto an ordinary finite Boolean cube.

Main definitions

• reindex: the function x ↦ f (fun i => x (e i)) on J → Bool.

Main results

• sensitivity_reindex: sensitivity (reindex e f) = sensitivity f.
• blockSensitivityAt_reindex: the block sensitivity of reindex e f at x equals the block sensitivity of f at fun i => x (e i).

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.reindex {I J : Type} (e : I ≃ J) (f : (I → Bool) → Bool) : (J → Bool) → Bool

Transport a Boolean function along an equivalence of its coordinate types.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) : sensitivity (reindex e f) = sensitivity f

Reindexing preserves sensitivity: sensitivity (reindex e f) = sensitivity f.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) (x : J → Bool) : blockSensitivityAt (reindex e f) x = blockSensitivityAt f fun (i : I) => x (e i)

The block sensitivity of reindex e f at x equals the block sensitivity of f at the pullback fun i => x (e i).