Closure properties of RP, coRP and ZPP

RP (Cslib.Complexity.RP) is closed under union and intersection, and so are coRP and ZPP = RP ∩ coRP Arora and Barak, Section 7.3. Both constructions run one-sided error deciders for the two problems on disjoint parts of the random string.

• Union. Accept when either decider accepts (Cslib.Complexity.orVerifier). On a member of one of the problems, its decider rejects at most half of its random strings, so the combined decider rejects at most half of all random strings (Cslib.Complexity.acceptCount_orVerifier); on a non-member of both, neither decider accepts.
• Intersection. Accept when both deciders accept (Cslib.Complexity.andVerifier). Error reduction makes each decider reject at most a quarter of the random strings on a member, so the combined decider accepts at least (3 / 4) ^ 2 ≥ 1 / 2 of them on a common member (Cslib.Complexity.acceptCount_andVerifier); on a non-member of either, one of them rejects.

A decider ignoring an empty random string shows P ⊆ RP; with closure of P under complement (Cslib.Complexity.compl_mem_P), P ⊆ coRP and P ⊆ ZPP. Since RP ⊆ NP, ZPP ⊆ NP ∩ coNP.

Main results

• Cslib.Complexity.P_subset_RP, Cslib.Complexity.P_subset_coRP, Cslib.Complexity.P_subset_ZPP.
• Cslib.Complexity.union_mem_RP, Cslib.Complexity.inter_mem_RP: RP is closed under union and intersection.
• Cslib.Complexity.union_mem_coRP, Cslib.Complexity.inter_mem_coRP, Cslib.Complexity.union_mem_ZPP, Cslib.Complexity.inter_mem_ZPP, Cslib.Complexity.diff_mem_ZPP, Cslib.Complexity.symmDiff_mem_ZPP, Cslib.Complexity.ZPP.booleanSubalgebra.
• Cslib.Complexity.ZPP_subset_NP_inter_coNP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Inclusions of P

theorem Cslib.Complexity.P_subset_RP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ RP enc

P ⊆ RP: a decider is a one-sided-error decider ignoring its random string, of length 0.

theorem Cslib.Complexity.P_subset_coRP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ coRP enc

P ⊆ coRP: P is closed under complement.

theorem Cslib.Complexity.P_subset_ZPP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ ZPP enc

P ⊆ ZPP, since ZPP = RP ∩ coRP.

theorem Cslib.Complexity.ZPP_subset_NP_inter_coNP {α : Type} {enc : α ↪ List Bool} : ZPP enc ⊆ NP enc ∩ coNP enc

ZPP ⊆ NP ∩ coNP.

Union and intersection

theorem Cslib.Complexity.union_mem_RP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ RP enc) (hB : B ∈ RP enc) : A ∪ B ∈ RP enc

RP is closed under union: accept when the decider for either problem accepts, on disjoint parts of the random string.

theorem Cslib.Complexity.inter_mem_RP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ RP enc) (hB : B ∈ RP enc) : A ∩ B ∈ RP enc

RP is closed under intersection: reduce the error of both deciders to 1 / 4, and accept when both accept, on disjoint parts of the random string.

theorem Cslib.Complexity.union_mem_coRP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ coRP enc) (hB : B ∈ coRP enc) : A ∪ B ∈ coRP enc

coRP is closed under union.

theorem Cslib.Complexity.inter_mem_coRP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ coRP enc) (hB : B ∈ coRP enc) : A ∩ B ∈ coRP enc

coRP is closed under intersection.

theorem Cslib.Complexity.inter_mem_ZPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ ZPP enc) (hB : B ∈ ZPP enc) : A ∩ B ∈ ZPP enc

ZPP is closed under intersection.

def Cslib.Complexity.ZPP.booleanSubalgebra {α : Type} (enc : α ↪ List Bool) : BooleanSubalgebra (Set α)

ZPP as a Boolean subalgebra of Set α.

@[simp]

theorem Cslib.Complexity.ZPP.coe_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} : ↑(booleanSubalgebra enc) = ZPP enc

@[simp]

theorem Cslib.Complexity.ZPP.mem_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ booleanSubalgebra enc ↔ A ∈ ZPP enc

theorem Cslib.Complexity.union_mem_ZPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ ZPP enc) (hB : B ∈ ZPP enc) : A ∪ B ∈ ZPP enc

ZPP is closed under union.

theorem Cslib.Complexity.diff_mem_ZPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ ZPP enc) (hB : B ∈ ZPP enc) : A \ B ∈ ZPP enc

ZPP is closed under set difference.

theorem Cslib.Complexity.symmDiff_mem_ZPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ ZPP enc) (hB : B ∈ ZPP enc) : symmDiff A B ∈ ZPP enc

ZPP is closed under symmetric difference.