Sensitivity separation: recursive profiles

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveProfiles.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

structure Complexity.BooleanAnalysis.Sensitivity.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 Complexity.BooleanAnalysis.Sensitivity.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

noncomputable def Complexity.BooleanAnalysis.Sensitivity.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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.Sensitivity.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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.Sensitivity.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.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.Sensitivity.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

theorem Complexity.BooleanAnalysis.Sensitivity.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

theorem Complexity.BooleanAnalysis.Sensitivity.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

theorem Complexity.BooleanAnalysis.Sensitivity.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

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.jointSensitivityAt_le_left {I : Type} [Fintype I] (f g : (I → Bool) → Bool) (x : I → Bool) : jointSensitivityAt f g x ≤ sensitivityAt f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.jointSensitivityAt_comm {I : Type} [Fintype I] (f g : (I → Bool) → Bool) (x : I → Bool) : jointSensitivityAt f g x = jointSensitivityAt g f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.jointSensitivity_one {I : Type} [Fintype I] (F : Fin 1 → (I → Bool) → Bool) (b : Bool) : jointSensitivity F b = 0