Formal target: Corpus.OEIS181546.conjecture

Conjecture: Given $F(n,L) = \sum_{k=0}^{\lfloor n/2 \rfloor} \binom{n-k}{k}^L$, then $\lim_{n\to\infty} F(n+1,L)/F(n,L) = (\mathrm{Fibonacci}(L)\sqrt{5} + \mathrm{Lucas}(L))/2$ for $L \ge 0$ where $\mathrm{Fibonacci}(n) = \mathrm{A000045}(n)$ and $\mathrm{Lucas}(n) = \mathrm{A000032}(n)$.

Exact formal statement

∀ (L : Nat),
  Filter.Tendsto.{0, 0}
    (fun n =>
      HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.OEIS181546.F (HAdd.hAdd.{0, 0, 0} n 1) L))
        (Nat.cast.{0} (Corpus.OEIS181546.F n L)))
    Filter.atTop.{0} (nhds.{0} (Corpus.OEIS181546.limitValue L))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record