Formal target: Corpus.Erdos1072.erdos_1072.variants.littleo

Erdős, Hardy, and Subbarao [HaSu02], believed that the number of $p \le x$ for which $f(p)=p−1$ is $o(x/\log x)$.

Exact formal statement

Asymptotics.IsLittleO.{0, 0, 0} Filter.atTop.{0}
  (fun x =>
    Nat.cast.{0}
      (Set.ncard.{0}
        (Inter.inter.{0}
          (Set.ofPred.{0} fun p => And (Nat.Prime p) (Eq.{1} (Corpus.Erdos1072.f p) (HSub.hSub.{0, 0, 0} p 1)))
          (Set.Icc.{0} 0 x))))
  fun x => HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} x) (Real.log (Nat.cast.{0} x))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record