Positive errors of clique approximators

On the complete graph on a set of k vertices, the approximate interpretation is wrong only when the exact value is true and the approximator says false. Plucking only adds acceptance, so such an error can only come from a conjunction whose two sets join to more than w vertices, all inside the k-set. Each such joined set lies inside at most C(n - w - 1, k - w - 1) of the k-sets, and a conjunction of two approximators has at most sunflowerBound p w ^ 2 pairs of sets (Cslib.Circuits.Monotone.Positive.scheme).

Main definitions

• Cslib.Circuits.Monotone.Positive.scheme: the approximation scheme on complete graphs.

Main results

• Cslib.Circuits.Monotone.Positive.card_superCliques: the number of k-sets containing a set.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Chapter 9

def Cslib.Circuits.Monotone.Positive.superCliques (n k : ℕ) (s : Finset (Fin n)) : Finset (Clique.CliqueSet n k)

The k-sets of vertices containing s.

@[simp]

theorem Cslib.Circuits.Monotone.Positive.mem_superCliques {n k : ℕ} {s : Finset (Fin n)} {c : Clique.CliqueSet n k} : c ∈ superCliques n k s ↔ s ⊆ ↑c

theorem Cslib.Circuits.Monotone.Positive.card_superCliques {n k : ℕ} {s : Finset (Fin n)} (hs : s.card ≤ k) : (superCliques n k s).card = (n - s.card).choose (k - s.card)

The number of k-sets containing a set s of at most k vertices.

theorem Cslib.Circuits.Monotone.Positive.card_superCliques_le {n k w : ℕ} (hk : w + 1 ≤ k) {s : Finset (Fin n)} (hs : w < s.card) : (superCliques n k s).card ≤ (n - (w + 1)).choose (k - (w + 1))

A set of more than w vertices lies inside at most C(n - w - 1, k - w - 1) of the k-sets.

def Cslib.Circuits.Monotone.Positive.andExceptions (n k w : ℕ) (F G : Finset (Finset (Fin n))) : Finset (Clique.CliqueSet n k)

The positive errors of a conjunction of two families: the k-sets containing a joined pair of more than w vertices.

theorem Cslib.Circuits.Monotone.Positive.card_andExceptions_le {n k w : ℕ} (hk : w + 1 ≤ k) (F G : Finset (Finset (Fin n))) : (andExceptions n k w F G).card ≤ F.card * G.card * (n - (w + 1)).choose (k - (w + 1))

def Cslib.Circuits.Monotone.Positive.errorCap (n k p w : ℕ) : ℕ

The number of positive errors charged to a conjunction.

def Cslib.Circuits.Monotone.Positive.errorCost (n k p w : ℕ) : signature.Op → ℕ

Only conjunctions make positive errors.

def Cslib.Circuits.Monotone.Positive.exceptions {p w : ℕ} (n k : ℕ) (op : Op) : (Fin (signature.Arity op) → Approximator n p w) → Finset (Clique.CliqueSet n k)

The positive errors of a gate.

theorem Cslib.Circuits.Monotone.Positive.card_exceptions_le {n k p w : ℕ} (hk : w + 1 ≤ k) (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) : (exceptions n k op A).card ≤ errorCost n k p w op

theorem Cslib.Circuits.Monotone.Positive.gate_correct {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 1 ≤ w) (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) (c : Clique.CliqueSet n k) (hc : c ∉ exceptions n k op A) : (interpretation op fun (i : Fin (signature.Arity op)) => (A i).decode (Clique.ofFinset ↑c)) ≤ (Approximator.interpretation op A).decode (Clique.ofFinset ↑c)

Away from its exceptions, a gate is positively correct on complete graphs.

def Cslib.Circuits.Monotone.Positive.scheme {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (hk : w + 1 ≤ k) : Approximation.Scheme interpretation Approximator.interpretation (fun (A : Approximator n p w) (c : Clique.CliqueSet n k) => A.decode (Clique.ofFinset ↑c)) (fun (c : Clique.CliqueSet n k) => Clique.ofFinset ↑c) Approximator.input

Positive errors. The approximation scheme on the complete graphs on k-sets: the approximate value is at least the exact one away from the exceptions of the conjunctions.