Superquadratic sensitivity separation: or

The OR orBits of finitely many bits and the disjunction orCopies f of Fintype.card K disjoint copies of a Boolean function f. Passing to orCopies f multiplies the sensitivity bound on rejected inputs and the block sensitivity at the all-false input by Fintype.card K, while the bound on accepted inputs is unchanged; this balances the zero and one sensitivities of the terminal predicate.

Main definitions

• orBits: disjunction of a finite family of bits.
• orCopies: disjunction of independent copies of a Boolean function, compose orBits f.

Main results

• sensitivity_orCopies_le: if f has sensitivity at most S₀ on rejected and at most S₁ on accepted inputs, then orCopies f has sensitivity at most max (Fintype.card K * S₀) S₁.
• card_le_blockSensitivityAt_orBits_zero: orBits has block sensitivity at least Fintype.card K at the all-false input.
• blockSensitivityAt_orCopies_zero: the block sensitivity of orCopies f at the all-false input is at least Fintype.card K times that of f.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.orBits {K : Type} [Fintype K] (x : K → Bool) : Bool

Disjunction of a finite family of Boolean values.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.orBits_eq_true {K : Type} [Fintype K] (x : K → Bool) : orBits x = true ↔ ∃ (k : K), x k = true

orBits x is true iff some coordinate of x is true.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.orBits_eq_false {K : Type} [Fintype K] (x : K → Bool) : orBits x = false ↔ ∀ (k : K), x k = false

orBits x is false iff every coordinate of x is false.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.orBits_zero {K : Type} [Fintype K] : (orBits fun (x : K) => false) = false

The OR of the all-false vector is false.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.orCopies {I K : Type} [Fintype K] (f : (I → Bool) → Bool) : (K × I → Bool) → Bool

Disjunction of independent copies of a Boolean function.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.orCopies_zero {I K : Type} [Fintype K] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) : (orCopies f fun (x : K × I) => false) = false

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity_orCopies_le {I K : Type} [Fintype K] [Fintype I] (f : (I → Bool) → Bool) (S₀ S₁ : ℕ) (h₀ : ∀ (x : I → Bool), f x = false → sensitivityAt f x ≤ S₀) (h₁ : ∀ (x : I → Bool), f x = true → sensitivityAt f x ≤ S₁) : sensitivity (orCopies f) ≤ max (Fintype.card K * S₀) S₁

If f has sensitivity at most S₀ at every rejected input and at most S₁ at every accepted input, then sensitivity (orCopies f) ≤ max (Fintype.card K * S₀) S₁.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.card_le_blockSensitivityAt_orBits_zero {K : Type} [Fintype K] : Fintype.card K ≤ blockSensitivityAt orBits fun (x : K) => false

The block sensitivity of orBits at the all-false input is at least Fintype.card K.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_orCopies_zero {I K : Type} [Fintype K] [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) : (Fintype.card K * blockSensitivityAt f fun (x : I) => false) ≤ blockSensitivityAt (orCopies f) fun (x : K × I) => false

If f rejects the all-false input, then Fintype.card K times the block sensitivity of f at the all-false input is at most the block sensitivity of orCopies f there.