Sensitivity separation: recursive one #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveOne.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.
theorem
Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_sensitivity_one_at
{k r h : ℕ}
{I : Type}
[Fintype I]
(T : Tournament k)
(label : Fin k → Fin k → Fin r)
(F : Fin (h + 1) → (I → Bool) → Bool)
(o : ℕ)
(ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o)
(q : Fin h)
(x : (Fin k × Fin r) × I → Bool)
(hx : recursiveFamily T label F q x = true)
:
sensitivityAt (recursiveFamily T label F q) x ≤ o * sideSensitivity F false + r * sideSensitivity F true
theorem
Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_side_one
{k r h : ℕ}
{I : Type}
[Fintype I]
(T : Tournament k)
(label : Fin k → Fin k → Fin r)
(F : Fin (h + 1) → (I → Bool) → Bool)
(o : ℕ)
(ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o)
:
sideSensitivity (recursiveFamily T label F) true ≤ o * sideSensitivity F false + r * sideSensitivity F true
theorem
Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_joint_one_at
{k r h : ℕ}
{I : Type}
[Fintype I]
(T : Tournament k)
(label : Fin k → Fin k → Fin r)
(F : Fin (h + 1) → (I → Bool) → Bool)
(hF : NestedFamily F)
(o : ℕ)
(ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o)
(q q' : Fin h)
(hqq : q < q')
(x : (Fin k × Fin r) × I → Bool)
(hx : recursiveFamily T label F q x = true)
(hx' : recursiveFamily T label F q' x = true)
:
jointSensitivityAt (recursiveFamily T label F q) (recursiveFamily T label F q') x ≤ o * jointSensitivity F false + r * sideSensitivity F true
theorem
Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_joint_one
{k r h : ℕ}
{I : Type}
[Fintype I]
(T : Tournament k)
(label : Fin k → Fin k → Fin r)
(F : Fin (h + 1) → (I → Bool) → Bool)
(hF : NestedFamily F)
(o : ℕ)
(ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o)
:
jointSensitivity (recursiveFamily T label F) true ≤ o * jointSensitivity F false + r * sideSensitivity F true