Documentation

Complexity.Computability.Circuit.Monotone.Clique.Positive

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 #

Main results #

References #

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

The k-sets of vertices containing s.

Instances For
    source
    @[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

    A k-set c belongs to superCliques n k s if and only if s ⊆ c.1.

    source
    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.

    source
    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.

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

      The number of positive errors charged to a conjunction.

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

        Only conjunctions make positive errors.

        Instances For
          source
          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.

          Instances For
            source
            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

            When w + 1 ≤ k, the number of positive exceptions at an op gate is at most errorCost n k p w op.

            source
            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.

            source
            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.

            Instances For