Formal target: Corpus.Erdos912.erdos_912

Prove that there exists some $c>0$ such that $$h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}$$ as $n\to \infty$.

Exact formal statement

Exists.{1} fun c =>
  And (GT.gt.{0} c 0)
    (Asymptotics.IsEquivalent.{0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (Corpus.Erdos912.h n)) fun n =>
      HMul.hMul.{0, 0, 0} c
        (HPow.hPow.{0, 0, 0} (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} n) (Real.log (Nat.cast.{0} n))) (1 / 2)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record