Series of reciprocal central binomial coefficients

DefinitionIntegrand of the antiderivative condition#✓fully proved

Let \(S\) be a sequence of real polynomials indexed by the natural numbers, with terms \(S(l)\). For a natural number \(l\) and a real number \(x\), the integrand is

\[\frac{8x^l - S(l)(x)}{\sqrt{x}\,(4 - x)},\]

where \(\sqrt{x} = 0\) for \(x < 0\) and a quotient with denominator \(0\) is \(0\).

noncomputable def TIntegrand (S : ℕ → Polynomial ℝ) (l : ℕ) (x : ℝ) : ℝ :=
  (8 * x ^ l - Polynomial.aeval x (S l)) / (Real.sqrt x * (4 - x))

Used by 1

Used byPolynomial family defined by an antiderivative

DefinitionPolynomial family defined by an antiderivative#✓fully proved

Let \(S\) and \(T\) be sequences of real polynomials indexed by the natural numbers, with terms \(S(l)\) and \(T(l)\). The pair \((S, T)\) satisfies this predicate when \(T(0) = 0\); for every \(l \ge 1\) the polynomial \(T(l)\) is nonzero and has degree \(l - 1\); and for every \(l \ge 1\) and every real \(x\) with \(0 < x < 4\), the function \(y \mapsto 2\sqrt{y}\,T(l)(y)\) is differentiable at \(x\) with derivative

\[\frac{8x^l - S(l)(x)}{\sqrt{x}\,(4 - x)}.\]

The term \(T(l)\) stands for the polynomial \(T_{l-1}\) of the source, so \(T(0) = 0\) encodes the convention \(T_{-1} = 0\), and the derivative condition expresses \(T_{l-1}(x)\) as \(\frac{1}{2\sqrt{x}}\) times an antiderivative of the displayed integrand.

def IsPolyTFamily (S T : ℕ → Polynomial ℝ) : Prop :=
  T 0 = 0 ∧
    (∀ l : ℕ, 1 ≤ l → (T l).natDegree = l - 1 ∧ T l ≠ 0) ∧
    ∀ l : ℕ, 1 ≤ l → ∀ x : ℝ, 0 < x → x < 4 →
      HasDerivAt (fun y : ℝ => 2 * Real.sqrt y * Polynomial.aeval y (T l))
        (TIntegrand S l x) x

Uses 1

Statement usesIntegrand of the antiderivative condition

TheoremMultisection formula for \(\sum_k x^k / \binom{2mk}{mk}\)#●ready to prove

Let \(m \ge 1\) be a natural number and \(x\) a complex number with \(|x| < 4^m\). Write \(H(y) = \sum_{n \ge 0} y^n / \binom{2n}{n}\), \(w = e^{2\pi i/m}\), and let \(x^{1/m}\) be the principal \(m\)-th root of \(x\). Then

\[ \sum_{k \ge 0} \frac{x^k}{\binom{2mk}{mk}} = \frac{1}{m} \sum_{j=0}^{m-1} H(w^j x^{1/m}). \]

public theorem_wanted tsum_div_centralBinom_mul_eq_multisection {m : ℕ} (hm : 1 ≤ m) {x : ℂ}
    (hx : ‖x‖ < 4 ^ m) :
    ∑' k : ℕ, x ^ k / (Nat.centralBinom (m * k) : ℂ) =
      (1 / m : ℂ) * ∑ j ∈ Finset.range m,
        ∑' n : ℕ, (Complex.exp (2 * Real.pi * Complex.I / m) ^ j * x ^ ((1 : ℂ) / m)) ^ n /
          (Nat.centralBinom n : ℂ)

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Theorem 7 (jis-2024-24.6.8-thm-7).

TheoremMultisection formula for \(\sum_k x^k / (k \binom{2mk}{mk})\)#●ready to prove

Let \(m \ge 1\) be a natural number and \(x\) a complex number with \(|x| < 4^m\). Write \(L(y) = \sum_{n \ge 1} y^n / (n \binom{2n}{n})\), \(w = e^{2\pi i/m}\), and let \(x^{1/m}\) be the principal \(m\)-th root of \(x\). Then

\[ \sum_{k \ge 1} \frac{x^k}{k \binom{2mk}{mk}} = \sum_{j=0}^{m-1} L(w^j x^{1/m}). \]

public theorem_wanted tsum_div_mul_centralBinom_mul_eq_multisection {m : ℕ} (hm : 1 ≤ m)
    {x : ℂ} (hx : ‖x‖ < 4 ^ m) :
    ∑' k : ℕ, x ^ (k + 1) / (((k + 1 : ℕ) : ℂ) * Nat.centralBinom (m * (k + 1))) =
      ∑ j ∈ Finset.range m,
        ∑' n : ℕ, (Complex.exp (2 * Real.pi * Complex.I / m) ^ j * x ^ ((1 : ℂ) / m)) ^ (n + 1) /
          (((n + 1 : ℕ) : ℂ) * Nat.centralBinom (n + 1))

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Theorem 8 (jis-2024-24.6.8-thm-8).

TheoremMultisection formula for \(\sum_k x^k / (k^2 \binom{2mk}{mk})\)#●ready to prove

Let \(m \ge 1\) be a natural number and \(x\) a complex number with \(|x| < 4^m\). Write \(K(y) = \sum_{n \ge 1} y^n / (n^2 \binom{2n}{n})\), \(w = e^{2\pi i/m}\), and let \(x^{1/m}\) be the principal \(m\)-th root of \(x\). Then

\[ \sum_{k \ge 1} \frac{x^k}{k^2 \binom{2mk}{mk}} = m \sum_{j=0}^{m-1} K(w^j x^{1/m}). \]

public theorem_wanted tsum_div_sq_mul_centralBinom_mul_eq_multisection {m : ℕ} (hm : 1 ≤ m)
    {x : ℂ} (hx : ‖x‖ < 4 ^ m) :
    ∑' k : ℕ, x ^ (k + 1) / (((k + 1 : ℕ) : ℂ) ^ 2 * Nat.centralBinom (m * (k + 1))) =
      (m : ℂ) * ∑ j ∈ Finset.range m,
        ∑' n : ℕ, (Complex.exp (2 * Real.pi * Complex.I / m) ^ j * x ^ ((1 : ℂ) / m)) ^ (n + 1) /
          (((n + 1 : ℕ) : ℂ) ^ 2 * Nat.centralBinom (n + 1))

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Theorem 10 (jis-2024-24.6.8-thm-10).

DefinitionClosed form of the reciprocal central binomial series#✓fully proved

For every real number \(x\), let

\[ H(x) = \frac{4\sqrt{x}\,\arcsin(\sqrt{x}/2)}{(4 - x)\sqrt{4 - x}} + \frac{4}{4 - x}. \]

The formula is meant for \(0 \le x < 4\), where by the paper \(H(x) = \sum_{n \ge 0} x^n / \binom{2n}{n}\).

noncomputable def centralBinomReciprocalH (x : ℝ) : ℝ :=
  4 * √x * Real.arcsin (√x / 2) / ((4 - x) * √(4 - x)) + 4 / (4 - x)

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Section 2.

Used by 3

Used byThe closed form \(H\) equals \(1\) at \(0\) · Antiderivative of \(x^l H(x)\) · Antiderivative of \(x^{l - 1/2} H(x)\)

TheoremThe closed form \(H\) equals \(1\) at \(0\)#✓fully proved

The function \(H(x) = \frac{4\sqrt{x}\,\arcsin(\sqrt{x}/2)}{(4 - x)\sqrt{4 - x}} + \frac{4}{4 - x}\) of a real variable satisfies \(H(0) = 1\).

theorem centralBinomReciprocalH_zero : centralBinomReciprocalH 0 = 1

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Section 2.

Uses 1

Statement usesClosed form of the reciprocal central binomial series

DefinitionCoefficients of Zurita's Q-polynomials#✓fully proved

For natural numbers \(l \ge 1\) and \(k\), the rational number \(q_k = q_{l,k}\) is given by \(q_l = -4/l\), by \(q_k = \frac{4k + 6}{k} q_{k+1}\) for \(1 \le k < l\), by \(q_0 = -12 q_1\), and by \(q_k = 0\) for \(k > l\). These are the coefficients of Zurita's polynomial \(Q_l\). For \(l = 0\) the definition gives \(q_{0,k} = 0\) for every \(k\).

def arcsinAntiderivQCoeff (l k : ℕ) : ℚ :=
  if l < k then 0
  else if k = 0 then -12 * ((-4 / l) * ∏ i ∈ Finset.Ico 1 l, ((4 * i + 6 : ℚ) / i))
  else (-4 / l) * ∏ i ∈ Finset.Ico k l, ((4 * i + 6 : ℚ) / i)

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1.

Used by 6

Used byZurita's arcsine antiderivative constants · The first two arcsine antiderivative constants · Zurita's Q-polynomials · Recursion for the coefficients of a Q-polynomial · Leading coefficient of a Q-polynomial · Constant coefficient of a Q-polynomial

TheoremLeading coefficient of a Q-polynomial#✓fully proved

For every natural number \(l \ge 1\), the coefficient \(q_l = q_{l,l}\) of \(x^l\) in Zurita's polynomial \(Q_l\) equals \(-4/l\).

theorem arcsinAntiderivQCoeff_self {l : ℕ} (hl : 1 ≤ l) : arcsinAntiderivQCoeff l l = -4 / l

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1.

Uses 1

Statement usesCoefficients of Zurita's Q-polynomials

TheoremRecursion for the coefficients of a Q-polynomial#✓fully proved

Write \(q_k = q_{l,k}\) for the coefficient of \(x^k\) in Zurita's polynomial \(Q_l\). For all natural numbers \(k\) and \(l\) with \(1 \le k < l\),

\[q_k = \frac{4k + 6}{k}\, q_{k+1}.\]

theorem arcsinAntiderivQCoeff_of_lt {l k : ℕ} (hk : 1 ≤ k) (hkl : k < l) :
    arcsinAntiderivQCoeff l k = (4 * k + 6) / k * arcsinAntiderivQCoeff l (k + 1)

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1.

Uses 1

Statement usesCoefficients of Zurita's Q-polynomials

TheoremConstant coefficient of a Q-polynomial#✓fully proved

For every natural number \(l \ge 1\), the constant coefficient \(q_0\) and the coefficient \(q_1\) of \(x\) in Zurita's polynomial \(Q_l\) satisfy \(q_0 = -12 q_1\).

theorem arcsinAntiderivQCoeff_zero {l : ℕ} (hl : 1 ≤ l) :
    arcsinAntiderivQCoeff l 0 = -12 * arcsinAntiderivQCoeff l 1

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1.

Uses 1

Statement usesCoefficients of Zurita's Q-polynomials

DefinitionZurita's Q-polynomials#✓fully proved

For a natural number \(l \ge 1\), \(Q_l\) is the polynomial with rational coefficients \(Q_l(x) = \sum_{i=0}^{l} q_i x^i\), where \(q_l = -4/l\), \(q_i = \frac{4i + 6}{i} q_{i+1}\) for \(1 \le i < l\), and \(q_0 = -12 q_1\). For \(l = 0\) it is the constant polynomial \(Q_0 = 8\).

noncomputable def arcsinAntiderivQ (l : ℕ) : ℚ[X] :=
  if l = 0 then C 8 else ∑ k ∈ Finset.range (l + 1), C (arcsinAntiderivQCoeff l k) * X ^ k

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1.

Uses 1 · Used by 1

Statement usesCoefficients of Zurita's Q-polynomials

Used byAntiderivative of \(x^l H(x)\)

DefinitionZurita's arcsine antiderivative constants#✓fully proved

For a natural number \(l \ge 1\), the rational constant \(C_l\) is \(C_l = -q_0/2\), where \(q_0\) is the constant coefficient of Zurita's polynomial \(Q_l\). For \(l = 0\) it is \(C_0 = -4\).

def arcsinAntiderivC (l : ℕ) : ℚ :=
  if l = 0 then -4 else -arcsinAntiderivQCoeff l 0 / 2

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1.

Uses 1 · Used by 2

Statement usesCoefficients of Zurita's Q-polynomials

Used byThe first two arcsine antiderivative constants · Antiderivative of \(x^l H(x)\)

TheoremThe first two arcsine antiderivative constants#✓fully proved

Zurita's constants satisfy \(C_1 = -24\) and \(C_2 = -120\), as in Table 1 of the paper.

theorem arcsinAntiderivC_one_two : arcsinAntiderivC 1 = -24 ∧ arcsinAntiderivC 2 = -120

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 1 and Table 1.

Uses 2

Statement usesZurita's arcsine antiderivative constants

Proof usesCoefficients of Zurita's Q-polynomials

DefinitionCoefficients of Zurita's polynomial \(S_l\)#✓fully proved

For natural numbers \(l\) and \(k\), the rational number \(s_k\) (which depends on \(l\)) is \(0\) when \(k > l\), and when \(k \le l\) it is \(s_k = \frac{8}{1 - 2l} \prod_{i=k}^{l-1} \frac{8(i + 1)}{2i - 1}\). Equivalently, \(s_l = 8/(1 - 2l)\) and \(s_k = \frac{8(k + 1)}{2k - 1} s_{k+1}\) for \(0 \le k < l\).

def arcsinAntiderivSCoeff (l k : ℕ) : ℚ :=
  if l < k then 0
  else 8 / (1 - 2 * l) * ∏ i ∈ Finset.Ico k l, (8 * ((i : ℚ) + 1) / (2 * i - 1))

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 3.

Used by 3

Used byZurita's S-polynomials · Recursion for the coefficients of an S-polynomial · Leading coefficient of an S-polynomial

TheoremLeading coefficient of an S-polynomial#✓fully proved

For every natural number \(l\), the coefficient \(s_l = s_{l,l}\) of \(x^l\) in Zurita's polynomial \(S_l\) equals \(8/(1 - 2l)\).

theorem arcsinAntiderivSCoeff_self (l : ℕ) : arcsinAntiderivSCoeff l l = 8 / (1 - 2 * l)

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 3.

Uses 1

Statement usesCoefficients of Zurita's polynomial \(S_l\)

TheoremRecursion for the coefficients of an S-polynomial#✓fully proved

Write \(s_k = s_{l,k}\) for the coefficient of \(x^k\) in Zurita's polynomial \(S_l\). For all natural numbers \(k\) and \(l\) with \(k < l\),

\[s_k = \frac{8(k + 1)}{2k - 1}\, s_{k+1}.\]

theorem arcsinAntiderivSCoeff_of_lt {l k : ℕ} (hkl : k < l) :
    arcsinAntiderivSCoeff l k =
      8 * ((k : ℚ) + 1) / (2 * k - 1) * arcsinAntiderivSCoeff l (k + 1)

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 3.

Uses 1

Statement usesCoefficients of Zurita's polynomial \(S_l\)

DefinitionZurita's S-polynomials#✓fully proved

For a natural number \(l\), \(S_l\) is the polynomial with rational coefficients \(S_l(x) = \sum_{i=0}^{l} s_i x^i\), where \(s_l = 8/(1 - 2l)\) and \(s_i = \frac{8(i + 1)}{2i - 1} s_{i+1}\) for \(0 \le i < l\).

noncomputable def arcsinAntiderivS (l : ℕ) : ℚ[X] :=
  ∑ k ∈ Finset.range (l + 1), C (arcsinAntiderivSCoeff l k) * X ^ k

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Definition 3.

Uses 1 · Used by 1

Statement usesCoefficients of Zurita's polynomial \(S_l\)

Used byAntiderivative of \(x^{l - 1/2} H(x)\)

TheoremAntiderivative of \(x^l H(x)\)#●ready to prove

Let \(l \ge 1\), let \(Q_l\) and \(C_l\) be Zurita's polynomial and constant, and let \(H\) be the closed form of the reciprocal central binomial series. Then there is a polynomial \(P\) with rational coefficients such that \(P(0) = 0\) and \(2(4 - x) P'(x) = 8x^l - Q_l(x)\) as polynomials. Moreover, for every such \(P\) and every real number \(x\) with \(0 < x < 4\), the real function

\[ F(y) = P(y) + C_l \arcsin(\sqrt{y}/2)^2 + \frac{\arcsin(\sqrt{y}/2)\,\sqrt{y}}{\sqrt{4 - y}}\, Q_l(y) \]

has derivative \(x^l H(x)\) at \(x\).

Such a \(P\) is unique: it is the paper's polynomial \(P_l\) (Definition 2), and \(F\) is an antiderivative of \(x^l H(x)\) on \(0 < x < 4\).

public theorem_wanted hasDerivAt_arcsinAntiderivP_pow_mul_centralBinomReciprocalH {l : ℕ}
    (hl : 1 ≤ l) :
    (∃ P : ℚ[X], P.eval 0 = 0 ∧
      2 * (C 4 - X) * derivative P = 8 * X ^ l - arcsinAntiderivQ l) ∧
    ∀ P : ℚ[X], P.eval 0 = 0 → 2 * (C 4 - X) * derivative P = 8 * X ^ l - arcsinAntiderivQ l →
      ∀ x : ℝ, 0 < x → x < 4 →
        HasDerivAt (fun y : ℝ => aeval y P + (arcsinAntiderivC l : ℝ) * Real.arcsin (√y / 2) ^ 2 +
            Real.arcsin (√y / 2) * √y / √(4 - y) * aeval y (arcsinAntiderivQ l))
          (x ^ l * centralBinomReciprocalH x) x

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Lemma 5 (jis-2024-24.6.8-lem-5).

Uses 3

Statement usesZurita's arcsine antiderivative constants · Zurita's Q-polynomials · Closed form of the reciprocal central binomial series

TheoremAntiderivative of \(x^{l - 1/2} H(x)\)#●ready to prove

Let \(l \ge 0\), let \(S_l\) be Zurita's polynomial, and let \(H\) be the closed form of the reciprocal central binomial series. Then there is a polynomial \(T\) with rational coefficients such that \((4 - x)(2x T'(x) + T(x)) = 8x^l - S_l(x)\) as polynomials. Moreover, for every such \(T\) and every real number \(x\) with \(0 < x < 4\), the real function

\[ G(y) = T(y)\sqrt{y} + \frac{\arcsin(\sqrt{y}/2)}{\sqrt{4 - y}}\, S_l(y) \]

has derivative \(\frac{x^l}{\sqrt{x}} H(x)\) at \(x\).

Such a \(T\) is unique: it is the paper's polynomial \(T_{l-1}\) (Definition 4, with \(T_{-1} = 0\)).

public theorem_wanted hasDerivAt_arcsinAntiderivT_pow_mul_centralBinomReciprocalH (l : ℕ) :
    (∃ T : ℚ[X], (C 4 - X) * (2 * X * derivative T + T) = 8 * X ^ l - arcsinAntiderivS l) ∧
    ∀ T : ℚ[X], (C 4 - X) * (2 * X * derivative T + T) = 8 * X ^ l - arcsinAntiderivS l →
      ∀ x : ℝ, 0 < x → x < 4 →
        HasDerivAt (fun y : ℝ => aeval y T * √y +
            Real.arcsin (√y / 2) / √(4 - y) * aeval y (arcsinAntiderivS l))
          (x ^ l / √x * centralBinomReciprocalH x) x

Sources

• Rimer Zurita, Elementary Functions Associated with Series Involving Reciprocals of Central Binomial Coefficients, Journal of Integer Sequences 27 (2024), Article 24.6.8, Lemma 6 (jis-2024-24.6.8-lem-6).

Uses 2

Statement usesZurita's S-polynomials · Closed form of the reciprocal central binomial series

DefinitionCoefficients of Zurita's polynomial \(S_n\)#✓fully proved

For a natural number \(n\), the rational numbers \(s_0, s_1, s_2, \dots\) are defined by \(s_0 = 1/(1/2 - n)\) and \(s_k = \frac{k - 1 - n}{k - n + 1/2}\, s_{k-1}\) for every \(k \ge 1\). Their first \(n + 1\) terms are the coefficients of \(S_n(x) = \sum_{k=0}^{n} s_k x^k\).

def zuritaSCoeff (n : ℕ) : ℕ → ℚ
  | 0 => 1 / (1 / 2 - n)
  | k + 1 => ((k : ℚ) - n) / ((k : ℚ) + 1 - n + 1 / 2) * zuritaSCoeff n k

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 1.

Used by 6

Used byZurita's series \(\sum_{k > n} 4^k x^k / ((k - n)\binom{2k}{k})\) · Zurita's series \(\sum_{k > n} 4^k x^k / ((k - n)^2\binom{2k}{k})\) · Zurita's constant \(c_n\) · Zurita's polynomial \(S_n\) · Values from Zurita's Tables 1-4 · Reversed coefficients of Zurita's polynomial \(T_{n-2}\)

DefinitionZurita's constant \(c_n\)#✓fully proved

For a natural number \(n\), let \(s_n\) be the coefficient of \(x^n\) in Zurita's polynomial \(S_n(x) = \sum_{k=0}^n s_k x^k\). Then \(c_n\) is the rational number \(s_n/2 - 1\). For \(n = 1\) this gives \(c_1 = 1\), the paper's convention.

def zuritaC (n : ℕ) : ℚ :=
  zuritaSCoeff n n / 2 - 1

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 2.

Uses 1 · Used by 3

Statement usesCoefficients of Zurita's polynomial \(S_n\)

Used byZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/(1-x)^{3/2}\) · Values from Zurita's Tables 1-4 · Reversed coefficients of Zurita's polynomial \(T_{n-2}\)

DefinitionReversed coefficients of Zurita's polynomial \(T_{n-2}\)#✓fully proved

Fix a natural number \(n\), let \(s_0, s_1, \dots\) be the coefficients of \(S_n\) and let \(c_n = s_n/2 - 1\). The rational numbers \(u_0, u_1, \dots\) are defined by \(u_0 = -s_{n-1}/2 - c_n\) and \(u_{i+1} = \frac{(k + 1 - n)\, u_i + s_k/2}{k - n}\) with \(k = n - 2 - i\), where the index subtractions \(n - 1\) and \(n - 2 - i\) are truncated at \(0\). For \(n \ge 2\) they list the coefficients of \(T_{n-2}\) backwards, \(t_{n-2-i} = u_i\) for \(0 \le i \le n - 2\); thus \(t_{n-2} = -s_{n-1}/2 - c_n\) and \(t_{k-1} = ((k + 1 - n) t_k + s_k/2)/(k - n)\) for \(k = n - 2, \dots, 1\).

def zuritaTCoeffRev (n : ℕ) : ℕ → ℚ
  | 0 => -zuritaSCoeff n (n - 1) / 2 - zuritaC n
  | i + 1 => ((((n - 2 - i : ℕ) : ℚ) + 1 - n) * zuritaTCoeffRev n i +
      zuritaSCoeff n (n - 2 - i) / 2) / (((n - 2 - i : ℕ) : ℚ) - n)

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 2.

Uses 2 · Used by 2

Statement usesZurita's constant \(c_n\) · Coefficients of Zurita's polynomial \(S_n\)

Used byValues from Zurita's Tables 1-4 · Coefficients of Zurita's polynomial \(T_{n-2}\)

DefinitionCoefficients of Zurita's polynomial \(T_{n-2}\)#✓fully proved

For natural numbers \(n\) and \(k\), \(t_k = u_{n-2-k}\), where \(n - 2 - k\) is truncated at \(0\) and \(u_0, u_1, \dots\) are the reversed coefficients of \(T_{n-2}\): with \(s_j\) the coefficients of \(S_n\) and \(c_n = s_n/2 - 1\), \(u_0 = -s_{n-1}/2 - c_n\) and \(u_{i+1} = ((m + 1 - n) u_i + s_m/2)/(m - n)\) for \(m = n - 2 - i\), the indices \(n - 1\) and \(n - 2 - i\) being truncated at \(0\). For \(k \le n - 2\) these are the coefficients of \(T_{n-2}(x) = \sum_{k=0}^{n-2} t_k x^k\); for \(k > n - 2\), \(t_k = u_0\).

def zuritaTCoeff (n k : ℕ) : ℚ :=
  zuritaTCoeffRev n (n - 2 - k)

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 2.

Uses 1 · Used by 3

Statement usesReversed coefficients of Zurita's polynomial \(T_{n-2}\)

Used byZurita's series \(\sum_{k > n} 4^k x^k / ((k - n)^2\binom{2k}{k})\) · Zurita's polynomial \(T_{n-2}\) · Values from Zurita's Tables 1-4

DefinitionZurita's coefficients \(m_k\)#✓fully proved

For a natural number \(n\), the rational numbers \(m_0, m_1, \dots\) are defined by \(m_0 = 2/(2n - 1)\) and \(m_k = \frac{2(k - n)}{2k - 2n + 1}\, m_{k-1}\) for \(k \ge 1\). Zurita's polynomial \(M_{n-1}\) is \(M_{n-1}(x) = \sum_{k=0}^{n-1} m_k x^k\).

def zuritaMCoeff (n : ℕ) : ℕ → ℚ
  | 0 => 2 / (2 * n - 1)
  | k + 1 => 2 * ((k : ℚ) + 1 - n) / (2 * ((k : ℚ) + 1) - 2 * n + 1) * zuritaMCoeff n k

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 3.

Used by 5

Used byZurita's series \(\sum_{k > n} 4^k x^k / ((k - n)^2\binom{2k}{k})\) · Zurita's constant \(d_n\) · Zurita's polynomial \(M_{n-1}\) · Coefficients of Zurita's polynomial \(N_{n-2}\) · Values from Zurita's Tables 1-4

DefinitionZurita's constant \(d_n\)#✓fully proved

For a natural number \(n\), let \(m_0, m_1, \dots\) be Zurita's coefficients, given by \(m_0 = 2/(2n - 1)\) and \(m_k = \frac{2(k - n)}{2k - 2n + 1}\, m_{k-1}\) for \(k \ge 1\), so that \(M_{n-1}(x) = \sum_{k=0}^{n-1} m_k x^k\) for \(n \ge 1\). Then \(d_n\) is the rational number \(m_{n-1}/2\) for \(n \ge 1\), and \(d_0 = m_0/2 = -1\). For \(n = 1\) this gives \(d_1 = 1\), the paper's convention.

def zuritaD (n : ℕ) : ℚ :=
  zuritaMCoeff n (n - 1) / 2

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 4.

Uses 1 · Used by 2

Statement usesZurita's coefficients \(m_k\)

Used byZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/\sqrt{1-x}\) · Values from Zurita's Tables 1-4

DefinitionCoefficients of Zurita's polynomial \(N_{n-2}\)#✓fully proved

For natural numbers \(n\) and \(k\), let \(m_k\) be Zurita's coefficient, given by \(m_0 = 2/(2n - 1)\) and \(m_k = \frac{2(k - n)}{2k - 2n + 1}\, m_{k-1}\) for \(k \ge 1\). This is the rational number \(m_k / (2(k - n + 1))\), taken to be \(0\) when \(k = n - 1\). For \(k \le n - 2\) it is the coefficient of \(x^k\) in \(N_{n-2}(x) = \frac12 \sum_{i=0}^{n-2} \frac{m_i x^i}{i - n + 1}\).

def zuritaNCoeff (n k : ℕ) : ℚ :=
  zuritaMCoeff n k / 2 / ((k : ℚ) - n + 1)

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 4.

Uses 1 · Used by 2

Statement usesZurita's coefficients \(m_k\)

Used byZurita's polynomial \(N_{n-2}\) · Values from Zurita's Tables 1-4

TheoremValues from Zurita's Tables 1-4#✓fully proved

For \(n = 2\) the coefficients \(s_0, s_1, s_2\) of \(S_2\) are \(-2/3\), \(-8/3\) and \(16/3\), and the constants \(c_2\) and \(c_4\) equal \(5/3\) and \(93/35\). For \(n = 3\) the coefficients \(t_0, t_1\) of \(T_1\) are \(-1/10\) and \(-3/5\), the coefficients \(m_0, m_1, m_2\) of \(M_2\) are \(2/5\), \(8/15\) and \(16/15\), the constant \(d_3\) equals \(8/15\), and the coefficients of \(x^0\) and \(x^1\) in \(N_1\) are \(-3/30\) and \(-8/30\).

In polynomial form: \(S_2(x) = -2/3 - (8/3)x + (16/3)x^2\), \(T_1(x) = -1/10 - (3/5)x\), \(M_2(x) = 2/5 + (8/15)x + (16/15)x^2\) and \(N_1(x) = -(8x + 3)/30\).

theorem zurita_table_values :
    (List.range 3).map (zuritaSCoeff 2) = [-2 / 3, -8 / 3, 16 / 3] ∧ zuritaC 2 = 5 / 3 ∧
      zuritaC 4 = 93 / 35 ∧ (List.range 2).map (zuritaTCoeff 3) = [-1 / 10, -3 / 5] ∧
      (List.range 3).map (zuritaMCoeff 3) = [2 / 5, 8 / 15, 16 / 15] ∧ zuritaD 3 = 8 / 15 ∧
      (List.range 2).map (zuritaNCoeff 3) = [-3 / 30, -8 / 30]

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Tables 1-4.

Uses 7

Statement usesZurita's constant \(c_n\) · Zurita's constant \(d_n\) · Zurita's coefficients \(m_k\) · Coefficients of Zurita's polynomial \(N_{n-2}\) · Coefficients of Zurita's polynomial \(S_n\) · Coefficients of Zurita's polynomial \(T_{n-2}\)

Proof usesReversed coefficients of Zurita's polynomial \(T_{n-2}\)

DefinitionZurita's polynomial \(S_n\)#✓fully proved

For a natural number \(n\) and a real number \(x\), \(S_n(x) = \sum_{k=0}^{n} s_k x^k\), where \(s_0 = 1/(1/2 - n)\) and \(s_k = \frac{k - 1 - n}{k - n + 1/2}\, s_{k-1}\) for \(k \ge 1\) are the coefficients of \(S_n\).

noncomputable def zuritaS (n : ℕ) (x : ℝ) : ℝ :=
  ∑ k ∈ range (n + 1), (zuritaSCoeff n k : ℝ) * x ^ k

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 1.

Uses 1 · Used by 2

Statement usesCoefficients of Zurita's polynomial \(S_n\)

Used byZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/(1-x)^{3/2}\) · Zurita's series \(\sum_{k > n} 4^k x^k / ((k - n)\binom{2k}{k})\)

DefinitionZurita's polynomial \(T_{n-2}\)#✓fully proved

For a natural number \(n\) and a real number \(x\), \(T_{n-2}(x) = \sum_{k=0}^{n-2} t_k x^k\), where \(t_0, t_1, \dots\) are the coefficients of Zurita's polynomial \(T_{n-2}\); for \(n \le 1\) the sum is empty and \(T_{n-2}(x) = 0\). For \(n \ge 2\) these coefficients are given by \(t_{n-2} = -s_{n-1}/2 - c_n\) and \(t_{k-1} = ((k + 1 - n) t_k + s_k/2)/(k - n)\) for \(k = n - 2, \dots, 1\), where \(s_0 = 1/(1/2 - n)\) and \(s_k = \frac{k - 1 - n}{k - n + 1/2}\, s_{k-1}\) for \(k \ge 1\) are the coefficients of Zurita's polynomial \(S_n\), and \(c_n = s_n/2 - 1\).

noncomputable def zuritaT (n : ℕ) (x : ℝ) : ℝ :=
  ∑ k ∈ range (n - 1), (zuritaTCoeff n k : ℝ) * x ^ k

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 2.

Uses 1 · Used by 2

Statement usesCoefficients of Zurita's polynomial \(T_{n-2}\)

Used byZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/(1-x)^{3/2}\) · Zurita's series \(\sum_{k > n} 4^k x^k / ((k - n)\binom{2k}{k})\)

DefinitionZurita's polynomial \(M_{n-1}\)#✓fully proved

For a natural number \(n\), let \(m_0, m_1, \dots\) be Zurita's coefficients, given by \(m_0 = 2/(2n - 1)\) and \(m_k = \frac{2(k - n)}{2k - 2n + 1}\, m_{k-1}\) for \(k \ge 1\). Then \(M_{n-1}\) is the real polynomial function \(M_{n-1}(x) = \sum_{k=0}^{n-1} m_k x^k\) (so \(M_{-1} = 0\)).

noncomputable def zuritaM (n : ℕ) (x : ℝ) : ℝ :=
  ∑ k ∈ range n, (zuritaMCoeff n k : ℝ) * x ^ k

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 3.

Uses 1 · Used by 2

Statement usesZurita's coefficients \(m_k\)

Used byZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/\sqrt{1-x}\) · Zurita's series \(\sum_{k > n} 4^k x^k / ((k - n)^2\binom{2k}{k})\)

DefinitionZurita's polynomial \(N_{n-2}\)#✓fully proved

For a natural number \(n\), let \(m_0, m_1, \dots\) be Zurita's coefficients, given by \(m_0 = 2/(2n - 1)\) and \(m_k = \frac{2(k - n)}{2k - 2n + 1}\, m_{k-1}\) for \(k \ge 1\). Then \(N_{n-2}\) is the real polynomial function \(N_{n-2}(x) = \frac12 \sum_{k=0}^{n-2} \frac{m_k x^k}{k - n + 1}\), which is \(0\) for \(n \le 1\).

noncomputable def zuritaN (n : ℕ) (x : ℝ) : ℝ :=
  ∑ k ∈ range (n - 1), (zuritaNCoeff n k : ℝ) * x ^ k

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Definition 4.

Uses 1 · Used by 1

Statement usesCoefficients of Zurita's polynomial \(N_{n-2}\)

Used byZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/\sqrt{1-x}\)

TheoremZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/(1-x)^{3/2}\)#●ready to prove

Let \(n \ge 1\), let \(c_n\) be Zurita's constant and let \(S_n\) and \(T_{n-2}\) be Zurita's polynomials (with \(T_{-1} = 0\)). For every real \(x\) with \(0 < x < 1\), the function

\[ F(y) = \log|y - 1| + c_n \log y + \frac{T_{n-2}(y)}{y^{n-1}} + \frac{\arcsin(\sqrt{y})\, S_n(y)}{y^{n-1/2} \sqrt{1 - y}} \]

has derivative \(x^{-n-1/2} \arcsin(\sqrt{x}) / (1 - x)^{3/2}\) at \(x\).

public theorem_wanted hasDerivAt_zurita_antiderivative_one {n : ℕ} (hn : 1 ≤ n) {x : ℝ}
    (hx0 : 0 < x) (hx1 : x < 1) :
    HasDerivAt (fun y => Real.log (y - 1) + (zuritaC n : ℝ) * Real.log y +
        zuritaT n y / y ^ (n - 1) +
        Real.arcsin (Real.sqrt y) * zuritaS n y / (y ^ ((n : ℝ) - 1 / 2) * Real.sqrt (1 - y)))
      (x ^ (-(n : ℝ) - 1 / 2) * Real.arcsin (Real.sqrt x) / (1 - x) ^ ((3 : ℝ) / 2)) x

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Lemma 1.

Uses 3

Statement usesZurita's constant \(c_n\) · Zurita's polynomial \(S_n\) · Zurita's polynomial \(T_{n-2}\)

TheoremZurita's antiderivative of \(x^{-n-1/2}\arcsin(\sqrt{x})/\sqrt{1-x}\)#●ready to prove

Let \(n \ge 1\), let \(d_n\) be Zurita's constant and let \(M_{n-1}\) and \(N_{n-2}\) be Zurita's polynomials (with \(N_{-1} = 0\)). For every real \(x\) with \(0 < x < 1\), the function

\[ G(y) = d_n \log y - \frac{\arcsin(\sqrt{y}) \sqrt{y(1 - y)}\, M_{n-1}(y)}{y^n} + \frac{N_{n-2}(y)}{y^{n-1}} \]

has derivative \(x^{-n-1/2} \arcsin(\sqrt{x}) / \sqrt{1 - x}\) at \(x\).

public theorem_wanted hasDerivAt_zurita_antiderivative_two {n : ℕ} (hn : 1 ≤ n) {x : ℝ}
    (hx0 : 0 < x) (hx1 : x < 1) :
    HasDerivAt (fun y => (zuritaD n : ℝ) * Real.log y -
        Real.arcsin (Real.sqrt y) * Real.sqrt (y * (1 - y)) * zuritaM n y / y ^ n +
        zuritaN n y / y ^ (n - 1))
      (x ^ (-(n : ℝ) - 1 / 2) * Real.arcsin (Real.sqrt x) / Real.sqrt (1 - x)) x

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Lemma 2.

Uses 3

Statement usesZurita's constant \(d_n\) · Zurita's polynomial \(M_{n-1}\) · Zurita's polynomial \(N_{n-2}\)

TheoremZurita's series \(\sum_{k > n} 4^k x^k / ((k - n)\binom{2k}{k})\)#●ready to prove

Let \(n \ge 1\), let \(S_n(x) = \sum_{k=0}^n s_k x^k\) and \(T_{n-2}\) be Zurita's polynomials (with \(T_{-1} = 0\)), and let \(x\) be real with \(0 < x < 1\). Then

\[ \sum_{k > n} \frac{4^k x^k}{(k - n)\binom{2k}{k}} = x\, T_{n-2}(x) + \sqrt{\frac{x}{1 - x}}\, \arcsin(\sqrt{x})\, S_n(x) + \sum_{k=0}^{n-1} \Bigl(1 - \frac{4^k}{\binom{2k}{k}}\Bigr) \frac{x^k}{k - n} - \Bigl(\frac12 \sum_{k=1}^{n} \frac{4^k s_{n-k}}{k \binom{2k}{k}}\Bigr) x^n. \]

The source prints the range \(|x| < 4\). The statement here is restricted to \(0 < x < 1\), inside the range \(|x| < 1\) that the source's Theorem 1 gives in this case; since \(\binom{2k}{k} \le 4^k\), the series diverges for \(x \ge 1\).

public theorem_wanted tsum_four_pow_div_sub_mul_centralBinom {n : ℕ} (hn : 1 ≤ n) {x : ℝ}
    (hx0 : 0 < x) (hx1 : x < 1) :
    ∑' k : ℕ, (4 : ℝ) ^ (k + n + 1) * x ^ (k + n + 1) /
        (((k : ℝ) + 1) * Nat.centralBinom (k + n + 1)) =
      x * zuritaT n x + Real.sqrt (x / (1 - x)) * Real.arcsin (Real.sqrt x) * zuritaS n x +
        ∑ k ∈ range n, (1 - (4 : ℝ) ^ k / Nat.centralBinom k) * x ^ k / ((k : ℝ) - n) -
        (1 / 2 * ∑ k ∈ Icc 1 n, (4 : ℝ) ^ k * (zuritaSCoeff n (n - k) : ℝ) /
          ((k : ℝ) * Nat.centralBinom k)) * x ^ n

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Corollary 1.

Uses 3

Statement usesZurita's polynomial \(S_n\) · Coefficients of Zurita's polynomial \(S_n\) · Zurita's polynomial \(T_{n-2}\)

TheoremZurita's series \(\sum_{k > n} 4^k x^k / ((k - n)^2\binom{2k}{k})\)#●ready to prove

For \(j \ge 1\) write Zurita's polynomials as \(S_j(x) = \sum_{k=0}^{j} s^{(j)}_k x^k\), \(T_{j-2}(x) = \sum_{k=0}^{j-2} t^{(j)}_k x^k\) and \(M_{j-1}(x) = \sum_{k=0}^{j-1} m^{(j)}_k x^k\). Let \(n \ge 1\), let \(x\) be real with \(0 < x < 1\), and put

\[ r_k = \frac{t^{(n)}_{k-1}}{k - n} + \frac{1}{2(k - n)} \sum_{l=0}^{k-1} s^{(n)}_l\, m^{(n-l)}_{k-l-1} + \frac{4^k}{(k - n)^2} \Bigl(4^{-k} - \frac{1}{\binom{2k}{k}}\Bigr) \]

for \(1 \le k \le n - 1\) and

\[ q = -\frac{2^{2n+1}}{\binom{2n}{n}} + \sum_{l=0}^{n-2} s^{(n)}_l \Bigl( \frac{4^{n-l}}{(n - l)\binom{2(n-l)}{n-l}} - \frac12 \sum_{p=1}^{n-l-1} \frac{4^p\, m^{(n-l)}_{n-l-1-p}}{p(2p + 1)\binom{2p}{p}}\Bigr). \]

Then

\[ \sum_{k > n} \frac{4^k x^k}{(k - n)^2 \binom{2k}{k}} = \frac{2^{2n+1} x^n}{\binom{2n}{n}} \arcsin(\sqrt{x})^2 - \arcsin(\sqrt{x}) \sqrt{x(1 - x)} \sum_{k=0}^{n-1} s^{(n)}_k M_{n-k-1}(x)\, x^k + \sum_{k=1}^{n-1} r_k x^k + q x^n. \]

MetaMathlibExt.tsum_four_pow_div_sub_sq_mul_centralBinom · 18 lines

public theorem_wanted tsum_four_pow_div_sub_sq_mul_centralBinom {n : ℕ} (hn : 1 ≤ n) {x : ℝ}
    (hx0 : 0 < x) (hx1 : x < 1) :
    let r : ℕ → ℝ := fun k =>
      ((zuritaTCoeff n (k - 1) : ℝ) / ((k : ℝ) - n) +
          1 / 2 * ∑ l ∈ range k, (zuritaSCoeff n l * zuritaMCoeff (n - l) (k - l - 1) : ℝ) /
            ((k : ℝ) - n)) +
        (4 : ℝ) ^ k / ((k : ℝ) - n) ^ 2 * (1 / (4 : ℝ) ^ k - 1 / Nat.centralBinom k)
    let q : ℝ := -(2 : ℝ) ^ (2 * n + 1) / Nat.centralBinom n +
      ∑ l ∈ range (n - 1), (zuritaSCoeff n l : ℝ) *
        ((4 : ℝ) ^ (n - l) / (((n - l : ℕ) : ℝ) * Nat.centralBinom (n - l)) -
          1 / 2 * ∑ p ∈ Icc 1 (n - l - 1), (4 : ℝ) ^ p * (zuritaMCoeff (n - l) (n - l - 1 - p) : ℝ) /
            ((p : ℝ) * (2 * p + 1) * Nat.centralBinom p))
    ∑' k : ℕ, (4 : ℝ) ^ (k + n + 1) * x ^ (k + n + 1) /
        (((k : ℝ) + 1) ^ 2 * Nat.centralBinom (k + n + 1)) =
      (2 : ℝ) ^ (2 * n + 1) * x ^ n / Nat.centralBinom n * Real.arcsin (Real.sqrt x) ^ 2 -
        Real.arcsin (Real.sqrt x) * Real.sqrt (x * (1 - x)) *
          ∑ k ∈ range n, (zuritaSCoeff n k : ℝ) * zuritaM (n - k) x * x ^ k +
        ∑ k ∈ Icc 1 (n - 1), r k * x ^ k + q * x ^ n

Sources

• Rimer Zurita, Power Series Associated with Reciprocals of Generalized Central Binomial Coefficients, INTEGERS 26 (2026), Article A2, Corollary 2.

Uses 4

Statement usesZurita's polynomial \(M_{n-1}\) · Zurita's coefficients \(m_k\) · Coefficients of Zurita's polynomial \(S_n\) · Coefficients of Zurita's polynomial \(T_{n-2}\)

27 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.