Formal target: Corpus.WikipediaElliottHalberstamConjecture.elliott_halberstam

The Elliott–Halberstam conjecture: for every $\theta < 1$ and $A > 0$ there exists a constant $C > 0$ such that $$\sum_{1 \le q \le x^{\theta}} E(x; q) \le \frac{C x}{\log^A x}$$ for all $x > 2$.

Exact formal statement

∀ (θ : Real),
  LT.lt.{0} θ 1 →
    ∀ (A : Real),
      LT.lt.{0} 0 A →
        Exists.{1} fun C =>
          And (GT.gt.{0} C 0)
            (∀ (x : Nat),
              LT.lt.{0} 2 x →
                LE.le.{0}
                  (Finset.sum.{0, 0} (Finset.Icc.{0} 1 (Nat.floor.{0} (HPow.hPow.{0, 0, 0} (Nat.cast.{0} x) θ)))
                    fun q => Corpus.WikipediaElliottHalberstamConjecture.E x q)
                  (HDiv.hDiv.{0, 0, 0} (HMul.hMul.{0, 0, 0} C (Nat.cast.{0} x))
                    (HPow.hPow.{0, 0, 0} (Real.log (Nat.cast.{0} x)) A)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record