Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.TournamentCounts

Sensitivity separation: tournament counts #

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

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

source
noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.internalEdges {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) :
Finset (Fin k × Fin k)

Directed edges whose two endpoints both belong to the given vertex set.

Equations
Instances For
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.card_internalEdges {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) :
    (T.internalEdges I).card = I.card.choose 2
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.sum_outdegree_eq {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) :
    ∑ i ∈ I, (Finset.filter (T.Adj i) I).card = (T.internalEdges I).card
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.card_le_three_of_outdegree_le_one {k : ℕ} (T : Tournament k) (I : Finset (Fin k)) (h : ∀ i ∈ I, (Finset.filter (T.Adj i) I).card ≤ 1) :
    I.card ≤ 3