Superquadratic sensitivity separation: basic

This file develops the elementary interface for flip, sensitivity and blockSensitivity: algebraic identities for flipping blocks (including on product index sets), upper and lower bound principles for the maxima defining sensitivity and block sensitivity, and the existence of inputs and block families attaining these maxima. It also shows that every nonconstant function has positive sensitivity.

Main results

• flip_flip: flipping the same block twice is the identity.
• flip_insert: for i ∉ B, flipping insert i B is flipping B and then {i}.
• exists_sensitivityAt_eq: the sensitivity of f is attained at some input.
• 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.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_empty {I : Type} (x : I → Bool) : flip x ∅ = x

Flipping the empty block leaves the input unchanged.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_singleton_self {I : Type} (x : I → Bool) (i : I) : flip x {i} i = !x i

Flipping {i} negates coordinate i.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_singleton_other {I : Type} (x : I → Bool) {i j : I} (h : j ≠ i) : flip x {i} j = x j

Flipping {i} leaves every coordinate j ≠ i unchanged.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_flip {I : Type} (x : I → Bool) (B : Finset I) : flip (flip x B) B = x

Flipping the same block twice gives back the original input.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_insert {I : Type} (x : I → Bool) (i : I) (B : Finset I) (hi : i ∉ B) : flip x (insert i B) = flip (flip x B) {i}

For i ∉ B, flipping insert i B equals flipping B and then {i}.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_prod_same {I J : Type} (x : J × I → Bool) (j : J) (i : I) : (fun (a : I) => flip x {(j, i)} (j, a)) = flip (fun (a : I) => x (j, a)) {i}

On the product index type J × I, row j of flip x {(j, i)} is row j of x with coordinate i flipped.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_prod_other {I J : Type} (x : J × I → Bool) {j k : J} (i : I) (hk : k ≠ j) : (fun (a : I) => flip x {(j, i)} (k, a)) = fun (a : I) => x (k, a)

On the product index type J × I, every row k ≠ j of flip x {(j, i)} equals row k of x.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.flip_false {I : Type} (B : Finset I) (i : I) : flip (fun (x : I) => false) B i = decide (i ∈ B)

Flipping a block B of the all-false input yields the indicator of B.

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.sensitivityAt_eq_zero_iff {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : sensitivityAt f x = 0 ↔ ∀ (i : I), f (flip x {i}) = f x

sensitivityAt f x = 0 iff no single-coordinate flip changes the value f x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.exists_sensitivityAt_eq {I : Type} [Fintype I] (f : (I → Bool) → Bool) : ∃ (x : I → Bool), sensitivityAt f x = sensitivity f

The sensitivity of f is attained: some input x has sensitivityAt f x = sensitivity f.

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.blockSensitivity_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) {n : ℕ} (h : ∀ (x : I → Bool), blockSensitivityAt f x ≤ n) : blockSensitivity f ≤ n

If blockSensitivityAt f x ≤ n for every input x, then blockSensitivity f ≤ n.

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 (flip x B) ≠ 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 (flip x B) ≠ 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 (flip x B) ≠ 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 (flip x (blocks k)) ≠ 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.