Formal target: Corpus.Erdos887.erdos_887.parts.ii

Is there an absolute constant $K$ such that, for every $C > 0$, if $n$ is sufficiently large then $n$ has at most $K$ divisors in $(n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})$.

Exact formal statement

Exists.{1} fun K =>
  ∀ (C : Real),
    GT.gt.{0} C 0 →
      Filter.Eventually.{0}
        (fun n =>
          LE.le.{0}
            (Finset.card.{0}
              (Finset.filter.{0} (fun d => Dvd.dvd.{0} d n)
                (Finset.Ioo.{0} (Nat.floor.{0} (Nat.cast.{0} n).sqrt)
                  (Nat.ceil.{0}
                    (HAdd.hAdd.{0, 0, 0} (Nat.cast.{0} n).sqrt
                      (HMul.hMul.{0, 0, 0} C (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) (1 / 4))))))))
            K)
        Filter.atTop.{0}

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record