Centered majority iteration preserves the bias interval
ProvedShiQMACenteredGap.biasIter_boundsamplificationqmaquantum-complexity
If an initial centered acceptance bias is between and , then every number of majority-of-three iterations leaves the bias in the same interval.
Preamble
import Definitions.Def_ShiQMACenteredGap set_option autoImplicit false open ShiQMAErrorIteration ShiQMACenteredGap
Formal statement
theorem ShiQMACenteredGap.biasIter_bounds {d : ℝ} (hd : 0 ≤ d) (hd' : d ≤ 1 / 2) (r : Nat) :
0 ≤ biasIter d r ∧ biasIter d r ≤ 1 / 2 := by sorrySource
Yueheng Shi, AMPUNI-centered-gap.lean, lines 22–68; context: Marriott and Watrous, Quantum Arthur–Merlin Games (2005), Section 3, Theorem 3, https://cs.uwaterloo.ca/~watrous/Papers/QuantumArthurMerlinGames.pdf