Sensitivity separation: labeling events

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/LabelingEvents.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.Tournament.labelingEvent {k r n : ℕ} (T : Tournament k) (v : Fin n → Fin k) (m : Fin n → Fin r) : Finset (Fin k × Fin k → Fin r)

Labelings whose edges between injected vertices have the prescribed target labels.

Equations

• T.labelingEvent v m = if Function.Injective v then {A : Fin k × Fin k → Fin r | ∀ (i j : Fin n), T.Adj (v i) (v j) → A (v i, v j) = m j} else ∅

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.mem_labelingEvent_iff {k r n : ℕ} (T : Tournament k) {v : Fin n → Fin k} {m : Fin n → Fin r} {A : Fin k × Fin k → Fin r} (hv : Function.Injective v) : A ∈ T.labelingEvent v m ↔ ∀ (i j : Fin n), T.Adj (v i) (v j) → A (v i, v j) = m j

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.labelingEvent_eq {k r n : ℕ} (T : Tournament k) [NeZero n] (v : Fin n → Fin k) (m : Fin n → Fin r) (hv : Function.Injective v) : T.labelingEvent v m = {A : Fin k × Fin k → Fin r | ∀ p ∈ T.internalEdges (Finset.image v Finset.univ), A p = m (Function.invFun v p.2)}

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.card_labelingEvent {k r n : ℕ} (T : Tournament k) [NeZero n] (v : Fin n → Fin k) (m : Fin n → Fin r) (hv : Function.Injective v) : (T.labelingEvent v m).card = r ^ (k * k - n.choose 2)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.card_labelingEvent_le {k r n : ℕ} (T : Tournament k) [NeZero n] (v : Fin n → Fin k) (m : Fin n → Fin r) : (T.labelingEvent v m).card ≤ r ^ (k * k - n.choose 2)

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.badLabelings {k : ℕ} (T : Tournament k) (n r : ℕ) : Finset (Fin k × Fin k → Fin r)

Union of labeling events over all vertex maps and target-label assignments.

Equations

• T.badLabelings n r = Finset.univ.biUnion fun (v : Fin n → Fin k) => Finset.univ.biUnion fun (m : Fin n → Fin r) => T.labelingEvent v m

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.labelingEvent_subset_bad {k r n : ℕ} (T : Tournament k) {v : Fin n → Fin k} {m : Fin n → Fin r} : T.labelingEvent v m ⊆ T.badLabelings n r

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.card_badLabelings_le {k r n : ℕ} (T : Tournament k) [NeZero n] : (T.badLabelings n r).card ≤ k ^ n * r ^ n * r ^ (k * k - n.choose 2)