doc(classes): docstrings for listed results and citations for problems and classes

Complexity/Computability/Communication/Protocol.lean

@@ -189,6 +189,8 @@ theorem exists_solves_depth_eq_ecomplexity (h : ∃ p : Protocol X Y Z, p.Solves
     (fun p : {p : Protocol X Y Z // p.Solves R A B} => (p.1.depth : ℕ∞))
   exact ⟨p, hp, hmin⟩
 
+/-- Upper bounds on communication complexity: `R` has communication complexity at most `k` on
+`A × B` exactly when some protocol of depth at most `k` solves it. -/
 theorem ecomplexity_le_iff {k : ℕ} :
     ecomplexity R A B ≤ k ↔ ∃ p : Protocol X Y Z, p.Solves R A B ∧ p.depth ≤ k := by
   constructor
@@ -228,10 +230,14 @@ theorem solves_univ_iff : p.Solves (fun x y z => f x y = z) Set.univ Set.univ 
 theorem ecomplexityFun_le_depth (hp : p.run = f) : ecomplexityFun f ≤ p.depth :=
   ecomplexity_le_depth (solves_univ_iff.mpr hp)
 
+/-- Computing `f` has communication complexity at most `k` exactly when some protocol of depth at
+most `k` computes `f`. -/
 theorem ecomplexityFun_le_iff {k : ℕ} :
     ecomplexityFun f ≤ k ↔ ∃ p : Protocol X Y Z, p.run = f ∧ p.depth ≤ k := by
   simp only [ecomplexityFun, ecomplexity_le_iff, solves_univ_iff]
 
+/-- Lower bounds on the communication complexity of `f` are lower bounds on the depth of every
+protocol computing `f`, including when there is none. -/
 theorem le_ecomplexityFun_iff {k : ℕ∞} :
     k ≤ ecomplexityFun f ↔ ∀ p : Protocol X Y Z, p.run = f → k ≤ p.depth := by
   simp only [ecomplexityFun, le_ecomplexity_iff, solves_univ_iff]

Complexity/Computability/Communication/RoundProtocol.lean

@@ -154,6 +154,8 @@ def comap (φ : X' → X) (ψ : Y' → Y) :
   | _, .alice send next => .alice (send ∘ φ) fun a => (next a).comap φ ψ
   | _, .bob send next => .bob (send ∘ ψ) fun a => (next a).comap φ ψ
 
+/-- Relabelling the inputs is precomposition: `P.comap φ ψ` outputs on `x` and `y` what `P` outputs
+on `φ x` and `ψ y`. -/
 @[simp] theorem run_comap (φ : X' → X) (ψ : Y' → Y) : ∀ {d : ℕ} (P : RoundProtocol X Y M Z d)
     (x : X') (y : Y'), (P.comap φ ψ).run x y = P.run (φ x) (ψ y)
   | _, .output _, _, _ => rfl
@@ -178,6 +180,8 @@ def ofProtocol : (p : Protocol X Y Z) → (d : ℕ) → p.depth ≤ d → RoundP
     cond b (ofProtocol p₁ d (le_of_max_le_right (Nat.le_of_succ_le_succ h)))
       (ofProtocol p₀ d (le_of_max_le_left (Nat.le_of_succ_le_succ h)))
 
+/-- A bit protocol of depth at most `d`, run as a round protocol with `d` messages, has the same
+output. -/
 @[simp] theorem run_ofProtocol : ∀ (p : Protocol X Y Z) (d : ℕ) (h : p.depth ≤ d) (x : X) (y : Y),
     (ofProtocol p d h).run x y = p.run x y
   | .output _, _, _, _, _ => rfl

Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean

@@ -293,6 +293,8 @@ private theorem mk_polyOfBits_one (l : List Bool) :
   · rw [List.length_append, List.length_singleton, List.length_concat, List.take_succ_cons]
     simp [bitEquiv_symm_true]
 
+/-- For a coefficient list `g = l ++ [true]` with top coefficient one, `modBits g f` is congruent
+to `f` modulo the polynomial of `g`: both have the same image in `AdjoinRoot (polyOfBits g)`. -/
 theorem mk_polyOfBits_modBits (l f : List Bool) :
     AdjoinRoot.mk (polyOfBits (l ++ [true])) (polyOfBits (modBits (l ++ [true]) f)) =
       AdjoinRoot.mk (polyOfBits (l ++ [true])) (polyOfBits f) := by
@@ -354,6 +356,8 @@ def isIrreducibleCode (m : ℕ) : Bool :=
   decide (2 ≤ m) && (List.range m).all fun d =>
     decide (d < 2) || decide (Nat.log 2 m / 2 < Nat.log 2 d) || (modBits d.bits m.bits).any id
 
+/-- **Trial division decides irreducibility**: `isIrreducibleCode m` holds exactly when the binary
+polynomial with code `m` is irreducible. -/
 theorem isIrreducibleCode_iff (m : ℕ) :
     isIrreducibleCode m = true ↔ Irreducible (polyOfCode m) := by
   unfold isIrreducibleCode

Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean

@@ -127,6 +127,8 @@ product `B u * B w`. -/
 def IsMulTable (B : Basis (Fin n) (ZMod 2) F) (tab : List (List (List Bool))) : Prop :=
   tab.length = n ∧ ∀ u w : Fin n, B u * B w = fieldOfBits B (tableEntry tab u w)
 
+/-- With a multiplication table of the basis `B`, `fieldMul` multiplies: the element with
+coordinates `fieldMul tab a b` is the product of those with coordinates `a` and `b`. -/
 theorem fieldOfBits_fieldMul {B : Basis (Fin n) (ZMod 2) F} {tab : List (List (List Bool))}
     (htab : IsMulTable B tab) (a b : List Bool) :
     fieldOfBits B (fieldMul tab a b) = fieldOfBits B a * fieldOfBits B b := by
@@ -229,6 +231,9 @@ private theorem fieldOfBits_foldl_esymmStep {B : Basis (Fin n) (ZMod 2) F}
     rw [List.foldl_cons, h2 j (by rw [hlen]; exact hj), List.map_cons, ← Multiset.cons_coe,
       Multiset.cons_add, Multiset.add_cons]
 
+/-- **The dynamic program for `e_t`**: with a multiplication table of the basis `B` and `0 < t`,
+`esymmCoords tab t zs` has the coordinates of the `t`-th elementary symmetric polynomial of the
+elements with coordinates `zs`. -/
 theorem fieldOfBits_esymmCoords {B : Basis (Fin n) (ZMod 2) F} {tab : List (List (List Bool))}
     (htab : IsMulTable B tab) {t : ℕ} (ht : 0 < t) (zs : List (List Bool)) :
     fieldOfBits B (esymmCoords tab t zs) = (↑(zs.map (fieldOfBits B)) : Multiset F).esymm t := by
@@ -258,6 +263,8 @@ elements. -/
 def traceBit (τ a : List Bool) : Bool :=
   ((List.range τ.length).map fun u => a.getD u false && τ.getD u false).foldl xor false
 
+/-- **The trace as a bit**: with a multiplication table of the basis `B`,
+`traceBit (traceVector tab) a` is the trace over `ZMod 2` of the element with coordinates `a`. -/
 theorem traceBit_traceVector {B : Basis (Fin n) (ZMod 2) F} {tab : List (List (List Bool))}
     (htab : IsMulTable B tab) (a : List Bool) :
     traceBit (traceVector tab) a = bitEquiv (Algebra.trace (ZMod 2) F (fieldOfBits B a)) := by

Complexity/Computability/Complexity/Classes/AWPP.lean

@@ -48,7 +48,8 @@ open Turing.MultiTapeTM
 
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
-/-- A GapP ratio in `[0, 1]`, at least `2/3` on members and at most `1/3` otherwise. -/
+/-- A GapP ratio in `[0, 1]`, at least `2/3` on members and at most `1/3` otherwise, Fenner's
+characterization of AWPP [Fenner][Fenner2003]. -/
 def AWPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ g ∈ GapP enc, ∃ p : Polynomial ℕ, ∀ a,
     (0 ≤ g a ∧ g a ≤ (2 : ℤ) ^ p.eval (enc a).length) ∧

Complexity/Computability/Complexity/Classes/BPP.lean

@@ -47,6 +47,7 @@ The probability is written as a count over the random strings, which are functio
 
 ## References
 
+* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977]
 * [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
 -/
 
@@ -72,7 +73,8 @@ def DecidesWithBoundedError (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : 
         V (a, List.ofFn r) = false).card)
 
 /-- The problems decided with bounded error by polynomial-time machines reading polynomially long
-random strings, with respect to the encoding `enc` of instances. -/
+random strings, with respect to the encoding `enc` of instances [Gill][Gill1977],
+[Arora and Barak, Section 7.1][AroraBarak09]. -/
 def BPP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTime V (encPair enc encBits) encBool ∧ DecidesWithBoundedError enc p V A}

Complexity/Computability/Complexity/Classes/BooleanHierarchy.lean

@@ -198,13 +198,14 @@ private theorem empty_mem_NP : (∅ : Set α) ∈ NP enc :=
 private theorem univ_mem_NP : (Set.univ : Set α) ∈ NP enc :=
   ⟨0, fun _ => true, .const _, by simp [IsVerifier]⟩
 
-/-- The `n`th level of the Boolean hierarchy over NP, with level zero containing only `∅`. -/
+/-- The `n`th level of the Boolean hierarchy over NP, with level zero containing only `∅`
+[Cai et al.][CaiEtAl1988]. -/
 def BH (enc : α ↪ List Bool) (n : ℕ) : Set (Set α) := differenceHierarchy (NP enc) n
 
 /-- The complement of the `n`th level of the Boolean hierarchy over NP. -/
 def coBH (enc : α ↪ List Bool) (n : ℕ) : Set (Set α) := {A | Aᶜ ∈ BH enc n}
 
-/-- The union of all finite levels of the Boolean hierarchy over NP. -/
+/-- The union of all finite levels of the Boolean hierarchy over NP [Cai et al.][CaiEtAl1988]. -/
 def BooleanHierarchy (enc : α ↪ List Bool) : Set (Set α) := ⋃ n, BH enc n
 
 /-- Every finite level belongs to the full Boolean hierarchy. -/
@@ -243,9 +244,11 @@ theorem coBH_zero : coBH enc 0 = {Set.univ} := by
   ext A
   simp [coBH, BH_zero, Set.compl_empty_iff]
 
+/-- The first level is precisely NP. -/
 @[simp]
 theorem BH_one : BH enc 1 = NP enc := differenceHierarchy_one _
 
+/-- The first dual level is precisely coNP. -/
 @[simp]
 theorem coBH_one : coBH enc 1 = coNP enc := by
   ext A

Complexity/Computability/Complexity/Classes/CeqP.lean

@@ -43,7 +43,9 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- `C=P`, the zero sets of integer-valued `GapP` functions. -/
+/-- `C=P`, the zero sets of integer-valued `GapP` functions
+[Fenner, Fortnow and Kurtz][FennerFortnowKurtz1994],
+[Fortnow, Classification 4.5][Fortnow1997]. -/
 def CeqP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ g ∈ GapP enc, ∀ a, a ∈ A ↔ g a = 0}
 

Complexity/Computability/Complexity/Classes/DP.lean

@@ -50,7 +50,8 @@ open Turing.MultiTapeTM
 
 variable {α β γ : Type} {enc : α ↪ List Bool} {A B : Set α}
 
-/-- The class of languages expressible as the intersection of an NP and a coNP language. -/
+/-- The class of languages expressible as the intersection of an NP and a coNP language
+[Papadimitriou][Papadimitriou94]. -/
 def DP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ B ∈ NP enc, ∃ C ∈ coNP enc, A = B ∩ C}
 

Complexity/Computability/Complexity/Classes/EXP.lean

@@ -69,7 +69,7 @@ open Turing Turing.MultiTapeTM Filter
 variable {α : Type*} {enc : α ↪ List Bool} {A : Set α}
 
 /-- The problems decidable within time `O(2 ^ n ^ k)` for some `k`, on instances whose encoding
-under `enc` has length `n`. -/
+under `enc` has length `n` [Arora and Barak, Section 2.6][AroraBarak09]. -/
 def EXP (enc : α ↪ List Bool) : Set (Set α) := ⋃ k, DTIME enc fun n => 2 ^ n ^ k
 
 theorem mem_EXP_iff : A ∈ EXP enc ↔ ∃ k, A ∈ DTIME enc fun n => 2 ^ n ^ k :=
@@ -83,7 +83,8 @@ theorem mem_E_iff : A ∈ E enc ↔ ∃ k, A ∈ DTIME enc fun n => 2 ^ (k * n)
   Set.mem_iUnion
 
 /-- The problems decidable by a nondeterministic machine within time `O(2 ^ n ^ k)` for some `k`,
-on instances whose encoding under `enc` has length `n`. -/
+on instances whose encoding under `enc` has length `n`
+[Arora and Barak, Section 2.6][AroraBarak09]. -/
 def NEXP (enc : α ↪ List Bool) : Set (Set α) := ⋃ k, NTIME enc fun n => 2 ^ n ^ k
 
 theorem mem_NEXP_iff : A ∈ NEXP enc ↔ ∃ k, A ∈ NTIME enc fun n => 2 ^ n ^ k :=
@@ -131,10 +132,12 @@ theorem NE_subset_NEXP : NE enc ⊆ NEXP enc := fun _ hA =>
 theorem NP_subset_NEXP {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ NEXP enc :=
   NP_subset_NE.trans NE_subset_NEXP
 
+/-- **Linear exponential time is within nondeterministic linear exponential time.** -/
 theorem E_subset_NE : E enc ⊆ NE enc := fun _ hA =>
   let ⟨k, hk⟩ := mem_E_iff.mp hA
   mem_NE_iff.mpr ⟨k, DTIME_subset_NTIME hk⟩
 
+/-- **Exponential time is within nondeterministic exponential time.** -/
 theorem EXP_subset_NEXP : EXP enc ⊆ NEXP enc := fun _ hA =>
   let ⟨k, hk⟩ := mem_EXP_iff.mp hA
   mem_NEXP_iff.mpr ⟨k, DTIME_subset_NTIME hk⟩

Complexity/Computability/Complexity/Classes/FewP.lean

@@ -51,7 +51,8 @@ open Turing.MultiTapeTM
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α}
 
 /-- A language in NP with a polynomial bound on the number of accepting certificates on every
-input. The bound is in the encoded input length, not in the certificate length. -/
+input [Allender and Rubinstein][AllenderRubinstein1988]. The bound is in the encoded input length,
+not in the certificate length. -/
 def FewP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, ∃ p : Polynomial ℕ,
     (∀ a, f a ≤ p.eval (enc a).length) ∧ ∀ a, a ∈ A ↔ 0 < f a}

Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean

@@ -29,6 +29,11 @@ which is `O(|x|)`. Padded descriptions are short.
   description with the number of binary digits of the length of the word.
 * `Cslib.Complexity.Diagonal.computableTidilyInO_shortDesc`: shortness is decided within quadratic
   time and linear space.
+
+## References
+
+* [M. Sipser, *Introduction to the Theory of Computation*, Theorems 9.3 and 9.10][Sipser2013]:
+  the padded descriptions in the proofs of the hierarchy theorems.
 -/
 
 @[expose] public section

Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean

@@ -520,6 +520,8 @@ theorem acceptProb_round_prover {x : Graph × Graph} (hx : x ∈ GraphNonIsomorp
   obtain ⟨σ, hσ⟩ := exists_equiv_of_mem_support_relabelDist hm hm'
   exact mem_GraphIsomorphism_iff.2 ⟨σ, hσ⟩
 
+/-- One round is an interactive proof for `GraphNonIsomorphism` with completeness `1` and
+soundness error `17 / 32`. -/
 theorem isInteractiveProof_round :
     IsInteractiveProof round GraphNonIsomorphism 1 (17 / 32) where
   complete x hx := ⟨prover x, (acceptProb_round_prover hx).ge⟩
@@ -537,6 +539,8 @@ theorem acceptProb_verifier_le {x : Graph × Graph} (hx : x ∈ GraphIsomorphism
     acceptProb (verifier x) P ≤ (17 / 32) ^ 2 :=
   acceptProb_sequentialRepeat_le (acceptProb_round_le hx) 2 P
 
+/-- The verifier, two sequential rounds, is an interactive proof for `GraphNonIsomorphism` with
+completeness `1` and soundness error `(17 / 32) ^ 2`. -/
 theorem isInteractiveProof_verifier :
     IsInteractiveProof verifier GraphNonIsomorphism 1 ((17 / 32) ^ 2) where
   complete x hx := ⟨prover x, (acceptProb_verifier_prover hx).ge⟩

Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean

@@ -61,6 +61,12 @@ All are polynomial-time in their unary or binary inputs.
 * `Cslib.Complexity.QBFProtocol.updatePt_canonPt`: updating a point.
 * `Cslib.Complexity.QBFProtocol.decodeReply_encodeReply`: decoding inverts the honest encoding.
 * `Cslib.Complexity.QBFProtocol.eval_sampleMod_le`: the samples are nearly uniform.
+
+## References
+
+* [A. Shamir, *IP = PSPACE*][Shamir1992]
+* [A. Shen, *IP = SPACE: simplified proof*][Shen1992]
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 8.3][AroraBarak09]
 -/
 
 @[expose] public section
@@ -106,6 +112,7 @@ theorem natCast_connectiveMod [NeZero p] (o : ArithQBF.Connective) (a b : ℕ) :
   · rw [connectiveMod, natCast_subMod, Nat.cast_mul, natCast_subMod, natCast_subMod,
       ArithQBF.Connective.apply, Nat.cast_one]
 
+/-- For `p ≠ 0`, `operatorMod` computes the operators of the arithmetization in `ZMod p`. -/
 theorem natCast_operatorMod [NeZero p] (o : ArithQBF.Operator) (t a b : ℕ) :
     ((operatorMod p o t a b : ℕ) : ZMod p) = o.apply (t : ZMod p) a b := by
   cases o
@@ -115,6 +122,8 @@ theorem natCast_operatorMod [NeZero p] (o : ArithQBF.Operator) (t a b : ℕ) :
   · rw [operatorMod, ZMod.natCast_mod, Nat.cast_add, Nat.cast_mul, Nat.cast_mul, natCast_subMod,
       ArithQBF.Operator.apply, Nat.cast_one]
 
+/-- For `p ≠ 0`, Horner's rule modulo `p` evaluates the coefficient list `l` at `z` in
+`ZMod p`. -/
 theorem natCast_hornerMod [NeZero p] (z : ℕ) (l : List ℕ) :
     ((hornerMod p z l : ℕ) : ZMod p) = evalCoeffList (z : ZMod p) (l.map Nat.cast) := by
   rw [hornerMod, List.foldl_reverse, Nat.sub_add_cancel NeZero.one_le]
@@ -188,6 +197,8 @@ theorem normPt_canonPt [NeZero p] (xs : List ℕ) (r : ℕ → ZMod p) :
   refine List.map_congr_left fun x hx => ?_
   rw [lookupPt_canonPt r hx, Nat.mod_eq_of_lt (ZMod.val_lt _)]
 
+/-- For `p ≠ 0`, setting the variable `v` to `z` in the point `r` on the variables of `xs` gives
+the point `Function.update r v z` on the same variables. -/
 theorem updatePt_canonPt [NeZero p] (xs : List ℕ) (r : ℕ → ZMod p) (v z : ℕ) :
     updatePt p xs (canonPt xs r) v z = canonPt xs (Function.update r v (z : ZMod p)) := by
   unfold updatePt canonPt

Complexity/Computability/Complexity/Classes/LogSpace.lean

@@ -107,7 +107,8 @@ variable {α β γ : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {e
   {A : Set α} {B : Set β} {C : Set γ}
 
 /-- The problems decided in logarithmic space with respect to the encoding `enc`: a Boolean
-function deciding membership is computable in logarithmic space. -/
+function deciding membership is computable in logarithmic space
+[Sipser, Section 8.4][Sipser2013]. -/
 def L (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f : α → Bool, ComputableInLogSpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true}
 

Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean

@@ -46,7 +46,8 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
-/-- The problems whose complements belong to native nondeterministic logarithmic space. -/
+/-- The problems whose complements belong to native nondeterministic logarithmic space
+[Sipser, Section 8.6][Sipser2013]. -/
 def coNL (enc : α ↪ List Bool) : Set (Set α) := {A | Aᶜ ∈ NL enc}
 
 /-- A problem belongs to `coNL` exactly when its complement belongs to `NL`. -/

Complexity/Computability/Complexity/Classes/ModP.lean

@@ -53,8 +53,8 @@ namespace Cslib.Complexity
 
 variable {α : Type} {enc : α ↪ List Bool} {A B : Set α} {k : ℕ}
 
-/-- For a fixed modulus `k`, languages recognized by a nonzero residue of a `#P` count. The
-standard modular counting classes use `k ≥ 2`. -/
+/-- For a fixed modulus `k`, languages recognized by a nonzero residue of a `#P` count
+[Fortnow, Classification 4.7][Fortnow1997]. The standard modular counting classes use `k ≥ 2`. -/
 def ModP (k : ℕ) (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ f ∈ SharpP enc, ∀ a, a ∈ A ↔ f a % k ≠ 0}
 

Complexity/Computability/Complexity/Classes/NP.lean

@@ -78,7 +78,7 @@ def IsVerifier (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Boo
   ∀ a, a ∈ A ↔ ∃ w : List Bool, w.length = p.eval (enc a).length ∧ V (a, w) = true
 
 /-- The problems with polynomial-time verifiers and polynomially long certificates, with respect to
-the encoding `enc` of instances. -/
+the encoding `enc` of instances [Arora and Barak, Definition 2.1][AroraBarak09]. -/
 def NP (enc : α ↪ List Bool) : Set (Set α) :=
   {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
     ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsVerifier enc p V A}
@@ -136,7 +136,7 @@ theorem IsVerifier.guard {c : α → Bool} (h : IsVerifier enc p V A) :
 
 end Padding
 
-/-- The problems whose complements are in `NP`. -/
+/-- The problems whose complements are in `NP` [Arora and Barak, Section 2.6][AroraBarak09]. -/
 def coNP (enc : α ↪ List Bool) : Set (Set α) := {A | Aᶜ ∈ NP enc}
 
 theorem mem_coNP {enc : α ↪ List Bool} {A : Set α} : A ∈ coNP enc ↔ Aᶜ ∈ NP enc := Iff.rfl

Complexity/Computability/Complexity/Classes/Operators.lean

@@ -63,7 +63,8 @@ variable {α : Type}
 open Classical in
 /-- **The parity operator `⊕·C`**: the problems `L` such that, for some `L' ∈ C` and polynomial
 `p`, `a ∈ L` exactly when an odd number of the strings `w` of length `p (enc a).length` have
-`(a, w) ∈ L'`. The problems of `C` are about pairs of an instance and a string. -/
+`(a, w) ∈ L'`. The problems of `C` are about pairs of an instance and a string
+[Toda][Toda1991]. -/
 def ParityOp (enc : α ↪ List Bool) (C : Set (Set (α × List Bool))) : Set (Set α) :=
   {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C,
     ∀ a, a ∈ L ↔ Odd (acceptCount (fun x => decide (x ∈ L')) a (p.eval (enc a).length))}
@@ -73,7 +74,7 @@ open Classical in
 polynomial `p`, membership in `L'` decides `L` with bounded error using random strings of length
 `p (enc a).length`: for every instance `a`, at least two thirds of the random strings `r` have
 `(a, r) ∈ L'` exactly when `a ∈ L`. The problems of `C` are about pairs of an instance and a
-string. -/
+string [Schöning][Schoening1989], [Toda][Toda1991]. -/
 def BPOp (enc : α ↪ List Bool) (C : Set (Set (α × List Bool))) : Set (Set α) :=
   {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, DecidesWithBoundedError enc p (fun x => decide (x ∈ L')) L}