Superquadratic sensitivity separation: recursive profiles

This file introduces the quantitative profiles tracked through the recursive construction. For a family F : Fin h → (I → Bool) → Bool of predicates, the side profile at b is the maximal sensitivity of a member of F at an input where it outputs b, and the joint profile at b is the maximal number of single-bit flips of one input that change two distinct members F q, F q' (with q < q') simultaneously while both output b.

Main definitions

• NestedFamily: a family of predicates whose acceptance sets shrink as the index grows.
• jointSensitivityAt: the number of coordinates whose flip changes both of two predicates.
• sideSensitivity: the maximal sensitivity over all indices and inputs with output b.
• jointSensitivity: the maximal joint sensitivity of F q and F q' over q < q' and inputs on which both output b.

Main results

• sideSensitivity_le: a uniform bound on sensitivities at inputs with output b bounds sideSensitivity F b.
• jointSensitivity_le: a uniform bound on the relevant joint sensitivities bounds jointSensitivity F b.
• jointSensitivityAt_le_left: joint sensitivity is at most the sensitivity of the first predicate.
• jointSensitivity_one: a family with a single member has joint profile 0.

References

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

structure Cslib.QueryComplexity.SensitivitySeparation.Internal.NestedFamily {h : ℕ} {I : Type} (F : Fin h → (I → Bool) → Bool) : Prop

Acceptance at a stronger index implies acceptance at every weaker index.

• accepts_of_le {q q' : Fin h} {x : I → Bool} : q ≤ q' → F q' x = true → F q x = true

  Weaker indices accept every input accepted at a stronger index.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.NestedFamily.rejects_of_le {h : ℕ} {I : Type} {F : Fin h → (I → Bool) → Bool} (hF : NestedFamily F) {q q' : Fin h} {x : I → Bool} (hqq : q ≤ q') (hx : F q x = false) : F q' x = false

In a nested family, rejection at index q implies rejection at every index q' ≥ q.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.jointSensitivityAt {I : Type} [Fintype I] (f g : (I → Bool) → Bool) (x : I → Bool) : ℕ

The number of coordinates whose one-bit flip changes both predicates.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.sideSensitivity {h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (b : Bool) : ℕ

Maximum sensitivity over all indices and inputs with the indicated output.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.jointSensitivity {h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (b : Bool) : ℕ

Maximum same-input, same-bit joint sensitivity over two distinct ordered indices.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sensitivityAt_le_sideSensitivity {h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (b : Bool) (q : Fin h) (x : I → Bool) (hx : F q x = b) : sensitivityAt (F q) x ≤ sideSensitivity F b

If F q x = b, then sensitivityAt (F q) x ≤ sideSensitivity F b.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.sideSensitivity_le {h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (b : Bool) (B : ℕ) (hB : ∀ (q : Fin h) (x : I → Bool), F q x = b → sensitivityAt (F q) x ≤ B) : sideSensitivity F b ≤ B

If sensitivityAt (F q) x ≤ B whenever F q x = b, then sideSensitivity F b ≤ B.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.jointSensitivityAt_le_jointSensitivity {h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (b : Bool) (q q' : Fin h) (x : I → Bool) (hqq : q < q') (hx : F q x = b) (hx' : F q' x = b) : jointSensitivityAt (F q) (F q') x ≤ jointSensitivity F b

If q < q' and F q x = F q' x = b, then jointSensitivityAt (F q) (F q') x ≤ jointSensitivity F b.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.jointSensitivity_le {h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (b : Bool) (B : ℕ) (hB : ∀ (q q' : Fin h) (x : I → Bool), q < q' → F q x = b → F q' x = b → jointSensitivityAt (F q) (F q') x ≤ B) : jointSensitivity F b ≤ B

If jointSensitivityAt (F q) (F q') x ≤ B whenever q < q' and F q x = F q' x = b, then jointSensitivity F b ≤ B.

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

The joint sensitivity of f and g at x is at most sensitivityAt f x.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.jointSensitivity_one {I : Type} [Fintype I] (F : Fin 1 → (I → Bool) → Bool) (b : Bool) : jointSensitivity F b = 0

A family indexed by Fin 1 has no two distinct indices, so its joint profile is 0.