Documentation

Complexity.Computability.Complexity.Classes.SharpP.Closure

Closure properties of #P and GapP #

#P (Cslib.Complexity.SharpP) is closed under addition and multiplication Arora and Barak, Chapter 17, so it is a subsemiring of the functions to ℕ (Cslib.Complexity.SharpP.subsemiring). Hence GapP (Cslib.Complexity.GapP), the differences of functions in #P, is closed under addition, negation and multiplication, a subring of the functions to ℤ (Cslib.Complexity.GapP.subring) Fenner, Fortnow and Kurtz.

For the sum f₁ + f₂, the first bit of a certificate chooses which verifier to run (Cslib.Complexity.selectVerifier); since the two verifiers read certificates of different lengths p₁(n) and p₂(n), each is padded to p₁(n) + p₂(n) bits by requiring the extra bits to be false (Cslib.Complexity.acceptCount_andVerifier_allFalseVerifier). For the product, the two verifiers read disjoint parts of the certificate (Cslib.Complexity.acceptCount_andVerifier).

Main definitions #

Main results #

References #

source
theorem Cslib.Complexity.SharpP.add_mem {α : Type} {enc : α ↪ List Bool} {f₁ f₂ : α → ℕ} (h₁ : f₁ ∈ SharpP enc) (h₂ : f₂ ∈ SharpP enc) :
f₁ + f₂ ∈ SharpP enc

#P is closed under addition: the first bit of a certificate chooses the verifier, and the bits that the chosen verifier does not read must be false.

source
theorem Cslib.Complexity.SharpP.mul_mem {α : Type} {enc : α ↪ List Bool} {f₁ f₂ : α → ℕ} (h₁ : f₁ ∈ SharpP enc) (h₂ : f₂ ∈ SharpP enc) :
f₁ * f₂ ∈ SharpP enc

#P is closed under multiplication: the two verifiers read disjoint parts of the certificate.

source
theorem Cslib.Complexity.SharpP.two_pow_mem {α : Type} {enc : α ↪ List Bool} (q : Polynomial ℕ) :
(fun (a : α) => 2 ^ Polynomial.eval (enc a).length q) ∈ SharpP enc

The function 2 ^ q(n), where n is the length of the encoded instance, is in #P: every certificate of length q(n) is accepted.

source
theorem Cslib.Complexity.SharpP.one_mem {α : Type} {enc : α ↪ List Bool} :
1 ∈ SharpP enc

The constant function 1 is in #P: the empty certificate is accepted.

source
def Cslib.Complexity.SharpP.subsemiring {α : Type} (enc : α ↪ List Bool) :
Subsemiring (α → ℕ)

#P as a subsemiring of the functions to ℕ.

Instances For
    source
    @[simp]
    theorem Cslib.Complexity.SharpP.coe_subsemiring {α : Type} {enc : α ↪ List Bool} :
    ↑(subsemiring enc) = SharpP enc
    source
    @[simp]
    theorem Cslib.Complexity.SharpP.mem_subsemiring {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} :
    f ∈ subsemiring enc ↔ f ∈ SharpP enc
    source
    theorem Cslib.Complexity.SharpP.add_one_mem {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (h : f ∈ SharpP enc) :
    f + 1 ∈ SharpP enc

    #P is closed under adding one.

    source
    theorem Cslib.Complexity.SharpP.natCast_mem {α : Type} {enc : α ↪ List Bool} (n : ℕ) :
    ↑n ∈ SharpP enc

    The constant functions are in #P.

    source
    theorem Cslib.Complexity.SharpP.pow_mem {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (h : f ∈ SharpP enc) (n : ℕ) :
    f ^ n ∈ SharpP enc

    #P is closed under powers.

    source
    theorem Cslib.Complexity.SharpP.two_pow_mul_mem {α : Type} {enc : α ↪ List Bool} (q : Polynomial ℕ) {f : α → ℕ} (h : f ∈ SharpP enc) :
    (fun (a : α) => 2 ^ Polynomial.eval (enc a).length q * f a) ∈ SharpP enc

    #P is closed under multiplication by 2 ^ q(n), where n is the length of the encoded instance.

    source
    theorem Cslib.Complexity.SharpP.sum_mem {α : Type} {enc : α ↪ List Bool} {ι : Type u_1} (s : Finset ι) {f : ι → α → ℕ} (h : ∀ i ∈ s, f i ∈ SharpP enc) :
    ∑ i ∈ s, f i ∈ SharpP enc

    #P is closed under finite sums.

    source
    theorem Cslib.Complexity.SharpP.prod_mem {α : Type} {enc : α ↪ List Bool} {ι : Type u_1} (s : Finset ι) {f : ι → α → ℕ} (h : ∀ i ∈ s, f i ∈ SharpP enc) :
    ∏ i ∈ s, f i ∈ SharpP enc

    #P is closed under finite products.

    source
    theorem Cslib.Complexity.SharpP.exists_two_pow_sub_mem {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (hf : f ∈ SharpP enc) :
    ∃ (p : Polynomial ℕ), (∀ (a : α), f a ≤ 2 ^ Polynomial.eval (enc a).length p) ∧ (fun (a : α) => 2 ^ Polynomial.eval (enc a).length p - f a) ∈ SharpP enc

    The complementary count: a function f in #P is at most 2 ^ p(n) for a polynomial p, where n is the length of the encoded instance, with 2 ^ p(n) - f also in #P: the negated verifier accepts the rejected certificates.

    source
    theorem Cslib.Complexity.SharpP.natCast_mem_GapP {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (hf : f ∈ SharpP enc) :
    (fun (a : α) => ↑(f a)) ∈ GapP enc

    A function in #P, cast to the integers, is in GapP.

    source
    theorem Cslib.Complexity.GapP.two_pow_mem {α : Type} {enc : α ↪ List Bool} (p : Polynomial ℕ) :
    (fun (a : α) => 2 ^ Polynomial.eval (enc a).length p) ∈ GapP enc

    A power of two with a length-polynomial exponent is in GapP.

    source
    theorem Cslib.Complexity.GapP.zero_mem {α : Type} {enc : α ↪ List Bool} :
    0 ∈ GapP enc

    The zero function is in GapP.

    source
    theorem Cslib.Complexity.GapP.one_mem {α : Type} {enc : α ↪ List Bool} :
    1 ∈ GapP enc

    The constant function 1 is in GapP.

    source
    theorem Cslib.Complexity.GapP.add_mem {α : Type} {enc : α ↪ List Bool} {g₁ g₂ : α → ℤ} (h₁ : g₁ ∈ GapP enc) (h₂ : g₂ ∈ GapP enc) :
    g₁ + g₂ ∈ GapP enc

    GapP is closed under addition.

    source
    theorem Cslib.Complexity.GapP.mul_mem {α : Type} {enc : α ↪ List Bool} {g₁ g₂ : α → ℤ} (h₁ : g₁ ∈ GapP enc) (h₂ : g₂ ∈ GapP enc) :
    g₁ * g₂ ∈ GapP enc

    GapP is closed under multiplication: (f₁ - f₂) (f₃ - f₄) = (f₁ f₃ + f₂ f₄) - (f₁ f₄ + f₂ f₃).

    source
    def Cslib.Complexity.GapP.subring {α : Type} (enc : α ↪ List Bool) :
    Subring (α → ℤ)

    GapP as a subring of the functions to ℤ.

    Instances For
      source
      @[simp]
      theorem Cslib.Complexity.GapP.coe_subring {α : Type} {enc : α ↪ List Bool} :
      ↑(subring enc) = GapP enc
      source
      @[simp]
      theorem Cslib.Complexity.GapP.mem_subring {α : Type} {enc : α ↪ List Bool} {g : α → ℤ} :
      g ∈ subring enc ↔ g ∈ GapP enc
      source
      theorem Cslib.Complexity.GapP.sub_mem' {α : Type} {enc : α ↪ List Bool} {g₁ g₂ : α → ℤ} (h₁ : g₁ ∈ GapP enc) (h₂ : g₂ ∈ GapP enc) :
      g₁ - g₂ ∈ GapP enc

      GapP is closed under subtraction.

      source
      theorem Cslib.Complexity.mem_SharpP_of_polyTime_length {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {r : α → ℕ} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) :
      (fun (a : α) => acceptCount V a (r a)) ∈ SharpP enc

      A polynomial-time unary certificate length can be padded without changing the count.

      source
      theorem Cslib.Complexity.SharpP.comp_mem {α : Type} {enc : α ↪ List Bool} {β : Type} {encB : β ↪ List Bool} {f : β → ℕ} {g : α → β} (hf : f ∈ SharpP encB) (hg : Turing.MultiTapeTM.ComputableInPolyTime g enc encB) :
      f ∘ g ∈ SharpP enc

      Polynomial-time precomposition preserves the exact accepting count. Padding bits are required to be false, so they do not multiply the number of witnesses.

      source
      theorem Cslib.Complexity.GapP.comp_mem {α : Type} {enc : α ↪ List Bool} {β : Type} {encB : β ↪ List Bool} {f : β → ℤ} {g : α → β} (hf : f ∈ GapP encB) (hg : Turing.MultiTapeTM.ComputableInPolyTime g enc encB) :
      f ∘ g ∈ GapP enc

      GapP is closed under polynomial-time precomposition.