Sensitivity separation: composition

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

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

def Complexity.BooleanAnalysis.Sensitivity.Internal.compose {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) : (I × J → Bool) → Bool

Block composition: evaluate the inner function in each row, then the outer function.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.compose f g x = f fun (i : I) => g fun (j : J) => x (i, j)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.compose_flip_sensitive_iff {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (x : I × J → Bool) (i : I) (j : J) : compose f g (flip x {(i, j)}) ≠ compose f g x ↔ (g (flip (fun (a : J) => x (i, a)) {j}) ≠ g fun (a : J) => x (i, a)) ∧ f (flip (fun (k : I) => g fun (a : J) => x (k, a)) {i}) ≠ f fun (k : I) => g fun (a : J) => x (k, a)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.compose_zero {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (hg : (g fun (x : J) => false) = false) : (compose f g fun (x : I × J) => false) = f fun (x : I) => false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.compose_flip_product_zero {I J : Type} (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (C : Finset I) (D : Finset J) (hg : (g fun (x : J) => false) = false) (hD : g (flip (fun (x : J) => false) D) ≠ g fun (x : J) => false) : compose f g (flip (fun (x : I × J) => false) (C ×ˢ D)) = f (flip (fun (x : I) => false) C)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivityAt_compose {I J : Type} [Fintype I] [Fintype J] (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (x : I × J → Bool) : sensitivityAt (compose f g) x = ∑ i : I with f (flip (fun (k : I) => g fun (a : J) => x (k, a)) {i}) ≠ f fun (k : I) => g fun (a : J) => x (k, a), sensitivityAt g fun (a : J) => x (i, a)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_compose_le {I J : Type} [Fintype I] [Fintype J] (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) : sensitivity (compose f g) ≤ sensitivity f * sensitivity g

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_compose_zero_le {I J : Type} [Fintype I] [Fintype J] (f : (I → Bool) → Bool) (g : (J → Bool) → Bool) (hg : (g fun (x : J) => false) = false) : ((blockSensitivityAt f fun (x : I) => false) * blockSensitivityAt g fun (x : J) => false) ≤ blockSensitivityAt (compose f g) fun (x : I × J) => false