Negative errors of clique approximators

On the complete multipartite graph of a colouring c with r colours, a set of vertices has all edges inside exactly when c is injective on it (Cslib.Circuits.Clique.contains_ofColoring_iff). The approximate interpretation is wrong on such an input only when the approximator says true and the exact value is false. Disjunctions and conjunctions of sets make no such errors; only plucking does, when the colouring is injective on the core of a sunflower but on none of its petals.

For such a colouring, every petal contains two vertices of the same colour, one of them outside the core and so private to the petal. Choosing such a pair for every petal fixes the colour of one private vertex per petal in terms of the colours of the others, which leaves at most (w ^ 2) ^ p * r ^ (n - p) colourings (card_sunflowerBad_le). A plucking normalisation makes at most as many plucks as the family has sets (Cslib.relatesInSteps_pluckNormalForm), which bounds the errors of a gate (Cslib.Circuits.Monotone.Negative.scheme).

On the other hand, a nonempty approximator accepts at least half of the colourings when r is at least twice the number w ^ 2 of pairs inside a set (half_le_card_acceptedColorings).

Main definitions

• Cslib.Circuits.Monotone.Negative.scheme: the approximation scheme on multipartite graphs.

Main results

• Cslib.Circuits.Monotone.Negative.card_sunflowerBad_le: the colourings injective on the core of a sunflower but on none of its petals.
• Cslib.Circuits.Monotone.Negative.half_le_card_acceptedColorings: a nonempty approximator accepts many colourings.

References

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

Colourings bad for a sunflower

def Cslib.Circuits.Monotone.Negative.collisionPairs {n : ℕ} (K s : Finset (Fin n)) : Finset (Fin n × Fin n)

The ordered pairs of distinct vertices of s whose first vertex is outside K.

@[simp]

theorem Cslib.Circuits.Monotone.Negative.mem_collisionPairs {n : ℕ} {K s : Finset (Fin n)} {uv : Fin n × Fin n} : uv ∈ collisionPairs K s ↔ uv.1 ∈ s ∧ uv.1 ∉ K ∧ uv.2 ∈ s ∧ uv.1 ≠ uv.2

theorem Cslib.Circuits.Monotone.Negative.card_collisionPairs_le {n w : ℕ} {K s : Finset (Fin n)} (hs : s.card ≤ w) : (collisionPairs K s).card ≤ w ^ 2

@[reducible, inline]

abbrev Cslib.Circuits.Monotone.Negative.Profile {n : ℕ} (S : Finset (Finset (Fin n))) (K : Finset (Fin n)) : Type

A choice of a collision pair in every petal.

theorem Cslib.Circuits.Monotone.Negative.card_profile_le {n w : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hS : ∀ s ∈ S, s.card ≤ w) : Fintype.card (Profile S K) ≤ (w ^ 2) ^ S.card

def Cslib.Circuits.Monotone.Negative.selected {n : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (π : Profile S K) : Finset (Fin n)

The first vertices of the pairs of a profile.

theorem Cslib.Circuits.Monotone.Negative.fst_injective {n : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hS : IsSunflower S K) (π : Profile S K) : Function.Injective fun (s : ↥S) => (↑(π s)).1

In a sunflower, the first vertex of a collision pair is private to its petal.

theorem Cslib.Circuits.Monotone.Negative.card_selected {n : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hS : IsSunflower S K) (π : Profile S K) : (selected π).card = S.card

theorem Cslib.Circuits.Monotone.Negative.snd_notMem_selected {n : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hS : IsSunflower S K) (π : Profile S K) (s : ↥S) : (↑(π s)).2 ∉ selected π

The second vertex of a collision pair is not selected.

def Cslib.Circuits.Monotone.Negative.profileColorings {n : ℕ} (r : ℕ) {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (π : Profile S K) : Finset (Clique.Coloring n r)

The colourings giving both vertices of every pair of a profile the same colour.

theorem Cslib.Circuits.Monotone.Negative.card_profileColorings_le {n r : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hS : IsSunflower S K) (π : Profile S K) : (profileColorings r π).card ≤ r ^ (n - S.card)

The colourings of a profile are determined by their colours outside the selected vertices.

theorem Cslib.Circuits.Monotone.Negative.exists_collisionPair {n r : ℕ} {c : Clique.Coloring n r} {K s : Finset (Fin n)} (hK : Set.InjOn c ↑K) (hs : ¬Set.InjOn c ↑s) : ∃ (uv : ↥(collisionPairs K s)), c (↑uv).1 = c (↑uv).2

A colouring injective on K but not on s has a collision pair in s.

def Cslib.Circuits.Monotone.Negative.sunflowerBad {n : ℕ} (r : ℕ) (S : Finset (Finset (Fin n))) (K : Finset (Fin n)) : Finset (Clique.Coloring n r)

The colourings injective on the core of a sunflower but on none of its petals.

def Cslib.Circuits.Monotone.Negative.pluckErrorCap (n r p w : ℕ) : ℕ

The number of negative errors charged to one pluck.

theorem Cslib.Circuits.Monotone.Negative.card_sunflowerBad_le {n r p w : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hSp : S.card = p) (hS : IsSunflower S K) (hSw : ∀ s ∈ S, s.card ≤ w) : (sunflowerBad r S K).card ≤ pluckErrorCap n r p w

Bad colourings of a sunflower. At most (w ^ 2) ^ p * r ^ (n - p) colourings are injective on the core of a sunflower with p petals of at most w vertices but on none of the petals.

Errors of plucking

noncomputable def Cslib.Circuits.Monotone.Negative.stepExceptions {n : ℕ} (r : ℕ) (F G : Finset (Finset (Fin n))) : Finset (Clique.Coloring n r)

The colourings accepted by G but not by F.

@[simp]

theorem Cslib.Circuits.Monotone.Negative.mem_stepExceptions {n r : ℕ} {F G : Finset (Finset (Fin n))} {c : Clique.Coloring n r} : c ∈ stepExceptions r F G ↔ Accepts G (Clique.ofColoring c) ∧ ¬Accepts F (Clique.ofColoring c)

theorem Cslib.Circuits.Monotone.Negative.card_stepExceptions_le_of_pluck {n r p w : ℕ} {F G : Finset (Finset (Fin n))} (h : Pluck p F G) (hF : ∀ s ∈ F, s.card ≤ w) : (stepExceptions r F G).card ≤ pluckErrorCap n r p w

One pluck makes at most pluckErrorCap n r p w negative errors.

theorem Cslib.Circuits.Monotone.Negative.stepExceptions_subset {n : ℕ} (r : ℕ) (F G H : Finset (Finset (Fin n))) : stepExceptions r F H ⊆ stepExceptions r F G ∪ stepExceptions r G H

theorem Cslib.Circuits.Monotone.Negative.card_stepExceptions_le_of_relatesInSteps {n r p w : ℕ} (hp : 2 ≤ p) {F G : Finset (Finset (Fin n))} {m : ℕ} (h : Relation.RelatesInSteps (Pluck p) F G m) (hF : ∀ s ∈ F, s.card ≤ w) : (stepExceptions r F G).card ≤ m * pluckErrorCap n r p w

m plucks make at most m times pluckErrorCap n r p w negative errors.

theorem Cslib.Circuits.Monotone.Negative.card_stepExceptions_pluckNormalForm_le {n r p w : ℕ} (hp : 2 ≤ p) {F : Finset (Finset (Fin n))} (hF : ∀ s ∈ F, s.card ≤ w) : (stepExceptions r F (pluckNormalForm p F)).card ≤ F.card * pluckErrorCap n r p w

A plucking normalisation makes at most as many errors as pluckErrorCap n r p w times the number of sets of the family.

The approximation scheme

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

The number of negative errors charged to each operation.

theorem Cslib.Circuits.Monotone.Negative.card_gateTerms_le {n r p w : ℕ} (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) : (gateTerms w op fun (i : Fin (signature.Arity op)) => (A i).terms).card * pluckErrorCap n r p w ≤ errorCost n r p w op

noncomputable def Cslib.Circuits.Monotone.Negative.exceptions {n p w : ℕ} (r : ℕ) (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) : Finset (Clique.Coloring n r)

The negative errors of a gate: those of plucking the sets produced at the gate.

theorem Cslib.Circuits.Monotone.Negative.gate_correct {n r p w : ℕ} [Fact (2 ≤ p)] (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) (c : Clique.Coloring n r) (hc : c ∉ exceptions r op A) : (Approximator.interpretation op A).decode (Clique.ofColoring c) ≤ interpretation op fun (i : Fin (signature.Arity op)) => (A i).decode (Clique.ofColoring c)

Away from its exceptions, a gate is negatively correct on multipartite graphs.

noncomputable def Cslib.Circuits.Monotone.Negative.scheme {n r p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) : Approximation.Scheme interpretation Approximator.interpretation (fun (A : Approximator n p w) (c : Clique.Coloring n r) => A.decode (Clique.ofColoring c)) Clique.ofColoring Approximator.input

Negative errors. The approximation scheme on the complete multipartite graphs of colourings with r colours: the approximate value is at most the exact one away from the errors of plucking.

Approximators accept many colourings

noncomputable def Cslib.Circuits.Monotone.Negative.acceptedColorings {n : ℕ} (r : ℕ) (F : Finset (Finset (Fin n))) : Finset (Clique.Coloring n r)

The colourings accepted by a family of vertex sets.

theorem Cslib.Circuits.Monotone.Negative.card_filter_not_injOn_le {n r w : ℕ} {s : Finset (Fin n)} (hs : s.card ≤ w) : {c : Clique.Coloring n r | ¬Set.InjOn c ↑s}.card ≤ w ^ 2 * r ^ (n - 1)

At most w ^ 2 * r ^ (n - 1) colourings are not injective on a set of at most w vertices.

theorem Cslib.Circuits.Monotone.Negative.half_le_card_acceptedColorings {n r w : ℕ} (hn : 0 < n) (hr : 2 * w ^ 2 ≤ r) {F : Finset (Finset (Fin n))} (hF : ∀ s ∈ F, s.card ≤ w) (hne : F.Nonempty) : r ^ n ≤ 2 * (acceptedColorings r F).card

Approximators accept many colourings. If r is at least twice w ^ 2, every nonempty family of sets of at most w vertices accepts at least half of the colourings.