Formal target: Corpus.Erdos243.erdos_243

Let $a_1 < a_2 < \dots$ be a sequence of integers such that $\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1$ and $\sum \frac{1}{a_n} \in \mathbb{Q}$.

Exact formal statement

∀ (a : Nat → Nat),
  StrictMono.{0, 0} a →
    Filter.Tendsto.{0, 0}
        (fun n =>
          HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (a n)) (HPow.hPow.{0, 0, 0} (Nat.cast.{0} (a (HSub.hSub.{0, 0, 0} n 1))) 2))
        Filter.atTop.{0} (nhds.{0} 1) →
      (Summable.{0, 0} fun x => HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} (a x))) →
        Filter.Eventually.{0}
          (fun n =>
            Eq.{1} (a n)
              (HAdd.hAdd.{0, 0, 0}
                (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} (a (HSub.hSub.{0, 0, 0} n 1)) 2)
                  (a (HSub.hSub.{0, 0, 0} n 1)))
                1))
          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