Sensitivity separation: basic

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

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

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_empty {I : Type} (x : I → Bool) : flip x ∅ = x

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_singleton_self {I : Type} (x : I → Bool) (i : I) : flip x {i} i = !x i

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_singleton_other {I : Type} (x : I → Bool) {i j : I} (h : j ≠ i) : flip x {i} j = x j

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_flip {I : Type} (x : I → Bool) (B : Finset I) : flip (flip x B) B = x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_insert {I : Type} (x : I → Bool) (i : I) (B : Finset I) (hi : i ∉ B) : flip x (insert i B) = flip (flip x B) {i}

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_prod_same {I J : Type} (x : J × I → Bool) (j : J) (i : I) : (fun (a : I) => flip x {(j, i)} (j, a)) = flip (fun (a : I) => x (j, a)) {i}

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_prod_other {I J : Type} (x : J × I → Bool) {j k : J} (i : I) (hk : k ≠ j) : (fun (a : I) => flip x {(j, i)} (k, a)) = fun (a : I) => x (k, a)

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_false {I : Type} (B : Finset I) (i : I) : flip (fun (x : I) => false) B i = decide (i ∈ B)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_differences {I : Type} [Fintype I] (x y : I → Bool) : flip x {i : I | x i ≠ y i} = y

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

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

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) {n : ℕ} (h : ∀ (x : I → Bool), sensitivityAt f x ≤ n) : sensitivity f ≤ n

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivityAt_eq_zero_iff {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : sensitivityAt f x = 0 ↔ ∀ (i : I), f (flip x {i}) = f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivityAt_pos {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) (i : I) (hi : f (flip x {i}) ≠ f x) : 0 < sensitivityAt f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.exists_sensitivityAt_eq {I : Type} [Fintype I] (f : (I → Bool) → Bool) : ∃ (x : I → Bool), sensitivityAt f x = sensitivity f

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_le_blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : blockSensitivityAt f x ≤ blockSensitivity f

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivity_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) {n : ℕ} (h : ∀ (x : I → Bool), blockSensitivityAt f x ≤ n) : blockSensitivity f ≤ n

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.le_blockSensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) (blocks : Finset (Finset I)) (hd : ∀ A ∈ blocks, ∀ B ∈ blocks, A ≠ B → Disjoint A B) (hb : ∀ B ∈ blocks, B.Nonempty ∧ f (flip x B) ≠ f x) : blocks.card ≤ blockSensitivityAt f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) {n : ℕ} (h : ∀ (blocks : Finset (Finset I)), (∀ A ∈ blocks, ∀ B ∈ blocks, A ≠ B → Disjoint A B) → (∀ B ∈ blocks, B.Nonempty ∧ f (flip x B) ≠ f x) → blocks.card ≤ n) : blockSensitivityAt f x ≤ n

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.exists_blockSensitivityAt_family {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : ∃ (blocks : Finset (Finset I)), blocks.card = blockSensitivityAt f x ∧ (∀ A ∈ blocks, ∀ B ∈ blocks, A ≠ B → Disjoint A B) ∧ ∀ B ∈ blocks, B.Nonempty ∧ f (flip x B) ≠ f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.le_blockSensitivityAt_of_family {I K : Type} [Fintype I] [Fintype K] (f : (I → Bool) → Bool) (x : I → Bool) (blocks : K → Finset I) (hne : ∀ (k : K), (blocks k).Nonempty) (hd : Pairwise fun (k l : K) => Disjoint (blocks k) (blocks l)) (hb : ∀ (k : K), f (flip x (blocks k)) ≠ f x) : Fintype.card K ≤ blockSensitivityAt f x

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.eq_of_singleton_invariant {I : Type} [Fintype I] (f : (I → Bool) → Bool) (h : ∀ (x : I → Bool) (i : I), f (flip x {i}) = f x) (x y : I → Bool) : f x = f y

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_pos_of_nonconstant {I : Type} [Fintype I] (f : (I → Bool) → Bool) (h : ∃ (x : I → Bool) (y : I → Bool), f x ≠ f y) : 0 < sensitivity f