Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.RecursiveSets

Sensitivity separation: recursive sets #

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

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

source
def Complexity.BooleanAnalysis.Sensitivity.Internal.childLift {J I : Type} (j : J) (A : Finset I) :
Finset (J × I)

Embed a coordinate block into a specified child of a product.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.mem_childLift {J I : Type} (j : J) (A : Finset I) (p : J × I) :
    p ∈ childLift j A ↔ p.1 = j ∧ p.2 ∈ A
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.childLift_card {J I : Type} (j : J) (A : Finset I) :
    (childLift j A).card = A.card
    source
    noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.childChanges {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) :
    Finset ((Fin k × Fin r) × I)

    Lift the individually sensitive coordinates of a child predicate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.childJointChanges {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q q' : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) :
      Finset ((Fin k × Fin r) × I)

      Lift coordinates that simultaneously change two predicates in one child.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.childChanges_card {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) :
        (childChanges F q x j c).card = sensitivityAt (F q) (recursiveChild x j c)
        source
        @[simp]
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.childJointChanges_card {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q q' : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) :
        (childJointChanges F q q' x j c).card = jointSensitivityAt (F q) (F q') (recursiveChild x j c)
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.card_biUnion_le_mul {J I : Type} [DecidableEq I] (A : Finset J) (B : J → Finset I) (n : ℕ) (hn : ∀ j ∈ A, (B j).card ≤ n) :
        (A.biUnion B).card ≤ A.card * n
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowClause_joint_flip_change {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q q' : Fin h) (x : (Fin k × Fin r) × I → Bool) (i j : Fin k) (c : Fin r) (a : I) (hc : rowClause T label F q (flip x {((j, c), a)}) i ≠ rowClause T label F q x i) (hc' : rowClause T label F q' (flip x {((j, c), a)}) i ≠ rowClause T label F q' x i) :
        j = i ∧ F (Fin.last h) (flip (recursiveChild x j c) {a}) ≠ F (Fin.last h) (recursiveChild x j c) ∨ T.Adj i j ∧ c = label i j ∧ F (gateIndex q) (flip (recursiveChild x j c) {a}) ≠ F (gateIndex q) (recursiveChild x j c) ∧ F (gateIndex q') (flip (recursiveChild x j c) {a}) ≠ F (gateIndex q') (recursiveChild x j c)