Formal target: Corpus.Erdos291.erdos_291.variants.shiu_heuristic_asymptotic

This leads to a heuristic prediction (see for example a preprint of Shiu [Sh16]) of $\asymp\frac{x}{\log x}$ for the number of $n\in [1,x]$ such that $(a_n,L_n)=1$.

Exact formal statement

Asymptotics.IsTheta.{0, 0, 0} Filter.atTop.{0}
  (fun x =>
    Nat.cast.{0}
      (Finset.card.{0}
        (Finset.filter.{0} (fun n => Eq.{1} ((Corpus.Erdos291.a n).gcd (Corpus.Erdos291.L n)) 1) (Finset.Icc.{0} 1 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