Franel numbers

DefinitionThe sequence A265233#✓fully proved

The sequence \((a_n)_{n \ge 0}\) of rational numbers is given by \(a_0 = 1\), \(a_1 = 1\), \(a_2 = 7\), \(a_3 = 56\) and, for every integer \(N \ge 4\),

\[N^2 a_N = (19N^2 - 19N + 6)\, a_{N-1} - 96 (N-1)^2 a_{N-2} + 144 (N-1)(N-2)\, a_{N-3}.\]

def a265233 : ℕ → ℚ
  | 0 => 1
  | 1 => 1
  | 2 => 7
  | 3 => 56
  | n + 4 =>
      ((19 * ((n : ℚ) + 4) ^ 2 - 19 * ((n : ℚ) + 4) + 6) *
          a265233 (n + 3)
        - 96 * ((n : ℚ) + 3) ^ 2 * a265233 (n + 2)
        + 144 * ((n : ℚ) + 3) * ((n : ℚ) + 2) *
          a265233 (n + 1))
        / ((n : ℚ) + 4) ^ 2

Sources

• Juntao Jin, "An Explicit Formula and a Recurrence for OEIS A265233", Theorem 1(2).

Used by 3

Used byExplicit formula for A265233 in terms of Franel numbers · Asymptotics of A265233 · Generating function of A265233

TheoremExplicit formula for A265233 in terms of Franel numbers#●ready to prove

Let \((a_n)_{n \ge 0}\) be the sequence A265233 and let \(f_m = \sum_{k=0}^{m} \binom{m}{k}^3\) be the \(m\)-th Franel number. For every integer \(n \ge 1\),

\[a_n = \frac{1}{6} \sum_{m=0}^{n} \binom{n}{m} 4^{n-m} f_m.\]

theorem_wanted a265233_eq_sum_franel (n : ℕ) (hn : 1 ≤ n) :
    a265233 n = (1 / 6) * ∑ m ∈ Finset.range (n + 1),
      (Nat.choose n m : ℚ) * 4 ^ (n - m) *
        (MetaMathlibExt.binomialPowerSeq 3 0 m : ℚ)

Sources

• Juntao Jin, "An Explicit Formula and a Recurrence for OEIS A265233", Theorem 1.

Uses 2

Statement usesThe sequence A265233 · Binomial-power sequences

TheoremFranel numbers as diagonal coefficients#●ready to prove

For every natural number \(m\), the coefficient of \(x^m y^m z^m\) in the polynomial \(\bigl((x + y)(y + z)(z + x)\bigr)^m \in \mathbb{Q}[x, y, z]\) is the Franel number \(f_m = \sum_{k=0}^{m} \binom{m}{k}^3\).

theorem_wanted coeff_pow_eq_franel (m : ℕ) :
    (((MvPolynomial.X 0 + MvPolynomial.X 1) *
        (MvPolynomial.X 1 + MvPolynomial.X 2) *
        (MvPolynomial.X 2 + MvPolynomial.X 0)) ^ m :
        MvPolynomial (Fin 3) ℚ).coeff
      (Finsupp.single (0 : Fin 3) m +
        Finsupp.single (1 : Fin 3) m +
        Finsupp.single (2 : Fin 3) m)
      = (MetaMathlibExt.binomialPowerSeq 3 0 m : ℚ)

Sources

• Juntao Jin, "An Explicit Formula and a Recurrence for OEIS A265233", Lemma 3.

Uses 1

Statement usesBinomial-power sequences

TheoremGenerating function of A265233#●ready to prove

Let \((a_n)_{n \ge 0}\) be the sequence A265233 and let \({}_2F_1\) be the Gauss hypergeometric function. For every real number \(x\) with \(|x| < 1/12\) and \(|27x(1 - 4x)^2| < 1\),

\[\sum_{n \ge 0} a_n x^n = \frac{{}_2F_1\bigl(\tfrac13, \tfrac23; 1; 27x(1 - 4x)^2\bigr) + 5}{6}.\]

theorem_wanted tsum_a265233_eq (x : ℝ) (hx : |x| < 1 / 12)
    (hz : |27 * x * (1 - 4 * x) ^ 2| < 1) :
    ∑' n : ℕ, (a265233 n : ℝ) * x ^ n =
      (ordinaryHypergeometric (1 / 3 : ℝ) (2 / 3 : ℝ) 1
        (27 * x * (1 - 4 * x) ^ 2) + 5) / 6

Sources

• Juntao Jin, "An Explicit Formula and a Recurrence for OEIS A265233", Corollary 2.

Uses 1

Statement usesThe sequence A265233

TheoremAsymptotics of A265233#●ready to prove

The sequence \((a_n)_{n \ge 0}\) A265233 satisfies

\[a_n \sim \frac{\sqrt{3}}{6\pi} \cdot \frac{12^n}{n} \quad \text{as } n \to \infty.\]

theorem_wanted a265233_isEquivalent :
    Asymptotics.IsEquivalent Filter.atTop
      (fun n : ℕ => (a265233 n : ℝ))
      (fun n : ℕ => Real.sqrt 3 / (6 * Real.pi) * 12 ^ n / n)

Sources

• Juntao Jin, "An Explicit Formula and a Recurrence for OEIS A265233", Corollary 2.

Uses 1

Statement usesThe sequence A265233

1 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.