Superquadratic sensitivity separation: iterates

Repeated disjoint composition iterateCompose f m of a Boolean function with itself, on the explicit coordinate type IterateCoord I m with Fintype.card I ^ m elements, and its reindexing iterateFin f m onto Fin (Fintype.card I ^ m). The sensitivity of the m-fold iterate is at most sensitivity f ^ m, while its block sensitivity at the all-false input is at least the m-th power of that of f.

Main definitions

• IterateCoord: coordinates I × (I × (⋯ × Unit)) of the m-fold iterate.
• iterateCompose: the m-fold block composition of f with itself.
• iterateFin: iterateCompose f m reindexed onto Fin (Fintype.card I ^ m).

Main results

• iterateCoord_card: IterateCoord I m has Fintype.card I ^ m elements.
• sensitivity_iterateFin_le: sensitivity (iterateFin f m) ≤ sensitivity f ^ m.
• blockSensitivityAt_iterateFin_zero: the block sensitivity of iterateFin f m at the all-false input is at least the m-th power of that of f.
• iterateFin_nonconstant: every iterate of a function with positive block sensitivity at the all-false input is nonconstant.

References

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

@[reducible, inline]

abbrev Cslib.QueryComplexity.SensitivitySeparation.Internal.IterateCoord (I : Type) : ℕ → Type

Coordinates of an iterated block composition, starting with a singleton.

@[instance_reducible]

instance Cslib.QueryComplexity.SensitivitySeparation.Internal.iterateCoordFintype {I : Type} [Fintype I] (m : ℕ) : Fintype (IterateCoord I m)

IterateCoord I m is finite whenever I is.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.iterateCompose {I : Type} (f : (I → Bool) → Bool) (m : ℕ) : (IterateCoord I m → Bool) → Bool

Repeated block composition of a Boolean function.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.iterateCoord_card {I : Type} [Fintype I] (m : ℕ) : Fintype.card (IterateCoord I m) = Fintype.card I ^ m

IterateCoord I m has Fintype.card I ^ m elements.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.iterateFin {I : Type} [Fintype I] (f : (I → Bool) → Bool) (m : ℕ) : (Fin (Fintype.card I ^ m) → Bool) → Bool

Reindex the iterated composition onto a finite ordinal.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.iterateFin_zero {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (m : ℕ) : (iterateFin f m fun (x : Fin (Fintype.card I ^ m)) => false) = false

If f rejects the all-false input, then so does iterateFin f m.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity_iterateFin_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) (m : ℕ) : sensitivity (iterateFin f m) ≤ sensitivity f ^ m

Sensitivity of reindexed iterates: sensitivity (iterateFin f m) ≤ sensitivity f ^ m.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_iterateFin_zero {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (m : ℕ) : (blockSensitivityAt f fun (x : I) => false) ^ m ≤ blockSensitivityAt (iterateFin f m) fun (x : Fin (Fintype.card I ^ m)) => false

If f rejects the all-false input, then the m-th power of its block sensitivity at the all-false input is at most the block sensitivity of iterateFin f m there.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.nonconstant_of_blockSensitivityAt_pos {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) (h : 0 < blockSensitivityAt f x) : ∃ (y : I → Bool) (z : I → Bool), f y ≠ f z

A Boolean function with positive block sensitivity at some input takes two distinct values.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.iterateFin_nonconstant {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (h : 0 < blockSensitivityAt f fun (x : I) => false) (m : ℕ) : ∃ (x : Fin (Fintype.card I ^ m) → Bool) (y : Fin (Fintype.card I ^ m) → Bool), iterateFin f m x ≠ iterateFin f m y

If f rejects the all-false input and has positive block sensitivity there, then every iterateFin f m takes two distinct values.