theorem Challenge.bombieri_vinogradov (A : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), 2 ≤ x → ∀ (Q : ℝ), 1 ≤ Q → Q ≤ √x / Real.log x ^ (A + 3) → ∑ q ∈ Finset.Icc 1 ⌊Q⌋₊, ⨆ y ∈ Set.Icc 1 x, ⨆ (a : (ZMod q)ˣ), |chebyPsi y ↑a - y / ↑q.totient| ≤ C * x / Real.log x ^ A