Repeated majority amplification preserves centered bias order
ProvedShiQMACenteredGap.biasIter_monoamplificationbiasqmaquantum-complexityschedule
For every round count, the iterated centered bias is monotone in an initial bias between zero and one half.
Preamble
import Definitions.Def_ShiQMACenteredGapGeneralSchedule import Theorems.Thm_ShiQMACenteredGap_biasStep_mono import Theorems.Thm_ShiQMACenteredGap_biasIter_bounds set_option autoImplicit false set_option maxHeartbeats 2000000 open ShiQMACenteredGap ShiQMAErrorIteration ShiQMAConstructiveSchedule
Formal statement
theorem ShiQMACenteredGap.biasIter_mono {d e : ℝ} (hd : 0 ≤ d) (hde : d ≤ e)
(he : e ≤ 1 / 2) (r : Nat) : biasIter d r ≤ biasIter e r := by sorrySource