Integer centering numerator represents the affine coin
ProvedShiQMACenteredGap.centeringNumerator_valueamplificationbinary-encodingcenteringqmaquantum-complexity
If two natural numerators A and B fit in k fractional bits, the integer centering numerator represents one minus the average of their dyadic values.
Preamble
import Definitions.Def_ShiQMACenteredGapComputableCoin set_option autoImplicit false
Formal statement
theorem ShiQMACenteredGap.centeringNumerator_value (k A B : Nat) (hA : A ≤ 2 ^ k) (hB : B ≤ 2 ^ k) :
(centeringNumerator k A B : ℝ) / (2 : ℝ) ^ (k + 1) =
1 - ((A : ℝ) / (2 : ℝ) ^ k + (B : ℝ) / (2 : ℝ) ^ k) / 2 := by
sorrySource