Sensitivity separation: tower profiles

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

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

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.towerSide {k r : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (D n : ℕ) (b : Bool) : ℕ

Maximum sensitivity on a given output side at a recursive tower level.

Equations

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

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.towerJoint {k r : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (D n : ℕ) (b : Bool) : ℕ

Maximum joint sensitivity on a given output side at a recursive tower level.

Equations

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

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerSide_zero {k r : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (D : ℕ) (b : Bool) : towerSide T label base D 0 b = sideSensitivity (base D) b

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerJoint_zero {k r : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (D : ℕ) (b : Bool) : towerJoint T label base D 0 b = jointSensitivity (base D) b

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.tower_four_recurrences {M r : ℕ} {I : Type} [Fintype I] (T : RegularTournament M) (A : GoodLabeling T.toTournament r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (D n : ℕ) (hn : n < D) (hr : 0 < r) (hbase : NestedFamily (base D)) : towerSide T.toTournament A.label base D (n + 1) true ≤ M ^ 2 * towerSide T.toTournament A.label base D n false + r * towerSide T.toTournament A.label base D n true ∧ towerJoint T.toTournament A.label base D (n + 1) true ≤ M ^ 2 * towerJoint T.toTournament A.label base D n false + r * towerSide T.toTournament A.label base D n true ∧ towerSide T.toTournament A.label base D (n + 1) false ≤ 16 * towerSide T.toTournament A.label base D n false + towerSide T.toTournament A.label base D n true + 3 * towerJoint T.toTournament A.label base D n true ∧ towerJoint T.toTournament A.label base D (n + 1) false ≤ 16 * towerSide T.toTournament A.label base D n false + 3 * towerJoint T.toTournament A.label base D n true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerBlocks_family_card {k r : ℕ} {I K : Type} [Fintype K] (blocks : K → Finset I) (hr : 0 < r) (hne : ∀ (b : K), (blocks b).Nonempty) (hd : Pairwise fun (a b : K) => Disjoint (blocks a) (blocks b)) (n : ℕ) : (Finset.image (towerBlocks blocks n) Finset.univ).card = k ^ n * Fintype.card K