Approximate a probability by a finite fair-bit coin
ProvedShiQMACenteredGap.exists_dyadic_coinamplificationcenteringqmaquantum-complexity
For every probability u in [0,1] and natural bit count k, some integer j between 0 and 2^k gives a dyadic probability j/2^k within 2^-k of u.
Preamble
import Mathlib.Data.Real.Archimedean import Mathlib.Data.Nat.Log set_option autoImplicit false
Formal statement
theorem ShiQMACenteredGap.exists_dyadic_coin {u : ℝ} (hu₀ : 0 ≤ u) (hu₁ : u ≤ 1) (k : Nat) :
∃ j : Nat, j ≤ 2 ^ k ∧
|(j : ℝ) / (2 : ℝ) ^ k - u| < 1 / (2 : ℝ) ^ k := by
sorrySource