Formal target: Corpus.OEIS105751.conjecture.variants.moll_p_mod_4_eq_1

Moll's conjecture 5.5 extends to this sequence and takes the form: (ii) for the other primes of type $2$, the p-adic valuation $\nu_p(a(n)) \sim n/(p - 1)$ as $n \rightarrow \infty$.

Exact formal statement

∀ {p : Nat},
  Nat.Prime p →
    Eq.{1} (HMod.hMod.{0, 0, 0} p 4) 1 →
      Filter.Tendsto.{0, 0}
        (fun n =>
          HDiv.hDiv.{0, 0, 0}
            (HMul.hMul.{0, 0, 0} (HSub.hSub.{0, 0, 0} (Nat.cast.{0} p) 1)
              (Nat.cast.{0} (padicValInt p (Corpus.OEIS105751.a n))))
            (Nat.cast.{0} n))
        Filter.atTop.{0} (nhds.{0} 1)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record