Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.RecursiveChildren

Sensitivity separation: recursive children #

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

Child positions used by a row clause, including its targets and outgoing gates.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowChildren_disjoint {k r : ℕ} (T : Tournament k) (label : Fin k → Fin k → Fin r) (i : Fin k) :
    Disjoint (Finset.image (fun (c : Fin r) => (i, c)) Finset.univ) (Finset.image (fun (j : Fin k) => (j, label i j)) (Finset.filter (T.Adj i) Finset.univ))
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowChildren_card {k r : ℕ} (T : Tournament k) (label : Fin k → Fin k → Fin r) (i : Fin k) :
    (rowChildren T label i).card = r + (Finset.filter (T.Adj i) Finset.univ).card
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.regular_rowChildren_card {M r : ℕ} (T : RegularTournament M) (label : Fin (2 * M ^ 2 + 1) → Fin (2 * M ^ 2 + 1) → Fin r) (i : Fin (2 * M ^ 2 + 1)) :
    (rowChildren T.toTournament label i).card = r + M ^ 2