P-recursive Sequence

Let $a_0,a_1,a_2,a_3,\cdots$ be a sequence of real numbers such that $a_0=0$, $a_1=1$, $a_2=8$, $a_3=41$, and $$a_{n+4}=\frac{(8n+29)a_{n+3}-(18n+63)a_{n+2}+27a_{n+1}+(27n+27)a_n}{n + 4}$$ for any natural number $n$. Prove that for any natural number $n$, $a_n$ is an integer.

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.33.0.

import Mathlib.Data.Set.Basic
import Mathlib.Data.Rat.Init

def a : ℕ → ℚ
  | 0 => 0
  | 1 => 1
  | 2 => 8
  | 3 => 41
  | n + 4 => ((8 * n + 29) * (a (n + 3)) - (18 * n + 63) * (a (n + 2)) +
      27 * (a (n + 1)) + (27 * n + 27) * (a n)) / (n + 4)

theorem solution {n : ℕ} : a n ∈ Set.range Int.cast := sorry

Submit Solution

Login to submit a solution.

Recent Submissions