Superquadratic sensitivity separation: reindex

Transport reindex e f of a Boolean function f along an equivalence e : I ≃ J of coordinate types. Sensitivity and block sensitivity, both pointwise and global, 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

• sensitivityAt_reindex: the sensitivity of reindex e f at x equals the sensitivity of f at fun i => x (e i).
• 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).
• blockSensitivity_reindex: blockSensitivity (reindex e f) = blockSensitivity f.

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.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.reindex_symm {I J : Type} (e : I ≃ J) (f : (I → Bool) → Bool) : reindex e.symm (reindex e f) = f

Reindexing along e and then along e.symm recovers the original function.

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

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

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).

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

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