Formal target: Corpus.Erdos394.erdos_394.variants.hall_conjecture

Erdős and Hall conjecture that the sum is $o(x^2/(\log x)^c)$ for any $c<\log 2$.

Exact formal statement

∀ (c : Real),
  LT.lt.{0} c (Real.log 2) →
    Asymptotics.IsLittleO.{0, 0, 0} Filter.atTop.{0}
      (fun x => Finset.sum.{0, 0} (Finset.Icc.{0} 1 (Nat.floor.{0} x)) fun n => Nat.cast.{0} (Corpus.Erdos394.t 2 n))
      fun x => HDiv.hDiv.{0, 0, 0} (HPow.hPow.{0, 0, 0} x 2) (HPow.hPow.{0, 0, 0} (Real.log x) c)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record