Superquadratic sensitivity separation: basic

This file develops the elementary interface for sensitivity and blockSensitivity: upper and lower bound principles for the maxima defining sensitivity and block sensitivity, the existence of block families attaining block sensitivity, and the fact that every nonconstant function has positive sensitivity.

Main results

• le_blockSensitivityAt_of_family: an indexed family of pairwise disjoint nonempty sensitive blocks at x bounds blockSensitivityAt f x from below by its size.
• exists_blockSensitivityAt_family: the block sensitivity at x is attained by a family of pairwise disjoint nonempty sensitive blocks.
• sensitivity_pos_of_nonconstant: a nonconstant function has positive sensitivity.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivityAt_le_card {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : sensitivityAt f x ≤ Fintype.card I

The sensitivity at any input is at most the number of coordinates Fintype.card I.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivityAt_le_sensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : sensitivityAt f x ≤ sensitivity f

The sensitivity at any input is at most sensitivity f.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivity_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) {n : ℕ} (h : ∀ (x : I → Bool), sensitivityAt f x ≤ n) : sensitivity f ≤ n

If sensitivityAt f x ≤ n for every input x, then sensitivity f ≤ n.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_le_blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : blockSensitivityAt f x ≤ blockSensitivity f

The block sensitivity at any input is at most blockSensitivity f.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.le_blockSensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) (blocks : Finset (Finset I)) (hd : ∀ A ∈ blocks, ∀ B ∈ blocks, A ≠ B → Disjoint A B) (hb : ∀ B ∈ blocks, B.Nonempty ∧ f (BitString.flipOn B x) ≠ f x) : blocks.card ≤ blockSensitivityAt f x

Every family of pairwise disjoint nonempty blocks, each of whose flips changes f x, has cardinality at most blockSensitivityAt f x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.blockSensitivityAt_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) {n : ℕ} (h : ∀ (blocks : Finset (Finset I)), (∀ A ∈ blocks, ∀ B ∈ blocks, A ≠ B → Disjoint A B) → (∀ B ∈ blocks, B.Nonempty ∧ f (BitString.flipOn B x) ≠ f x) → blocks.card ≤ n) : blockSensitivityAt f x ≤ n

If every family of pairwise disjoint nonempty blocks whose flips all change f x has at most n members, then blockSensitivityAt f x ≤ n.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.exists_blockSensitivityAt_family {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : ∃ (blocks : Finset (Finset I)), blocks.card = blockSensitivityAt f x ∧ (∀ A ∈ blocks, ∀ B ∈ blocks, A ≠ B → Disjoint A B) ∧ ∀ B ∈ blocks, B.Nonempty ∧ f (BitString.flipOn B x) ≠ f x

The block sensitivity at x is attained by a family of pairwise disjoint nonempty blocks, each of whose flips changes f x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.le_blockSensitivityAt_of_family {I K : Type} [Fintype I] [Fintype K] (f : (I → Bool) → Bool) (x : I → Bool) (blocks : K → Finset I) (hne : ∀ (k : K), (blocks k).Nonempty) (hd : Pairwise fun (k l : K) => Disjoint (blocks k) (blocks l)) (hb : ∀ (k : K), f (BitString.flipOn (blocks k) x) ≠ f x) : Fintype.card K ≤ blockSensitivityAt f x

Indexed form of le_blockSensitivityAt: if blocks : K → Finset I consists of nonempty, pairwise disjoint blocks whose flips all change f x, then Fintype.card K ≤ blockSensitivityAt f x.

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

A function taking two different values has positive sensitivity.