Uniform gap amplification for SBP

The powering argument for multiplicative gap amplification in [Wat12], Sections 1.1 and 3, works uniformly for polynomial-time unary repetition counts. A fixed dominating length polynomial also handles any polynomially bounded requested exponent, even when that request is not itself computable. The witness remains #P, and the positive threshold remains polynomial-time with binary output. This is gap amplification, not an additive error bound on a normalized acceptance probability.

Main results

• exists_SBP_gap_pow_polyTime: a positive unary polynomial-time exponent gives a uniform gap.
• exists_SBP_gap_pow_polyBounded: a polynomially bounded requested exponent gives a uniform gap.

References

• T. Watson, The Complexity of Estimating Min-Entropy, Sections 1.1 and 3.

theorem Cslib.Complexity.exists_SBP_gap_pow_polyTime {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ SBP enc) {r : α → ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) (hpos : ∀ (a : α), 0 < r a) : ∃ f ∈ SharpP enc, ∃ (k : α → ℕ), Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encNat ∧ (∀ (a : α), 0 < k a) ∧ ∀ (a : α), (a ∈ A → k a ≤ f a) ∧ (a ∉ A → 2 ^ r a * f a < k a)

Uniform SBP gap strengthening by positive, polynomial-time unary powers. Both the #P numerator and the positive binary-output threshold are raised to the same input-dependent power.

theorem Cslib.Complexity.exists_SBP_gap_pow_polyBounded {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ SBP enc) (r : α → ℕ) (hr : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) r) : ∃ f ∈ SharpP enc, ∃ (k : α → ℕ), Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encNat ∧ (∀ (a : α), 0 < k a) ∧ ∀ (a : α), (a ∈ A → k a ≤ f a) ∧ (a ∉ A → 2 ^ r a * f a < k a)

Uniform SBP amplification. One #P witness and one positive polynomial-time binary threshold achieve gap 2 ^ r(a) for every polynomially bounded requested exponent. The request need not be computable: the proof uses a fixed length polynomial dominating it, plus one to ensure positive repetition even when the request is zero.