Arcsine series and central binomial sums

TheoremLehmer's central binomial series for arcsin#✓fully proved

For every real number \(x\) with \(|x| < 1\), the series

\[\sum_{m=1}^{\infty} \frac{(2x)^{2m}}{m \binom{2m}{m}}\]

converges unconditionally, and its sum is \(\dfrac{2x}{\sqrt{1 - x^2}} \arcsin x\).

The source attributes the identity to D. H. Lehmer.

theorem arcsin_central_binomial_reciprocal_series
    (x : ℝ)
    (hx : |x| < 1) :
    HasSum (fun m : ℕ =>
        (2 * x) ^ (2 * (m + 1)) / ((↑(m + 1) : ℝ) * ↑(Nat.choose (2 * (m + 1)) (m + 1))))
      ((2 * x / Real.sqrt (1 - x ^ 2)) * Real.arcsin x)

Sources

• B. Sury, Tianming Wang, and Feng-Zhen Zhao, "Identities Involving Reciprocals of Binomial Coefficients," Journal of Integer Sequences 7 (2004), Article 04.2.8, Theorem, lines 365–371, https://cs.uwaterloo.ca/journals/JIS/VOL7/Sury/sury99.tex

Used by 1

Used byEntry 22 of Chapter 9 of Ramanujan's notebooks

DefinitionNormalized central binomial coefficient#✓fully proved

For a natural number \(n\), the normalized central binomial coefficient is the real number \(c_n = \binom{2n}{n}/2^{2n} = \binom{2n}{n}/4^n\).

def centralBinomialCoeff (n : ℕ) : ℝ :=
  (Nat.choose (2 * n) n : ℝ) / (2 : ℝ) ^ (2 * n)

Used by 14

Used byIntegrated arcsine series · Terms of the integrated arcsine series · The integrated arcsine series vanishes at the origin · Arcsine Taylor series · Taylor series of the arcsine · Normalized central binomial coefficients are at most one · Normalized central binomial coefficients are nonnegative · Continuity of the integrated arcsine series · Derivative of the integrated arcsine series · Bound on the terms of the integrated arcsine series · Summability of the integrated arcsine series · Summability of the arcsine series · The central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

LemmaNormalized central binomial coefficients are nonnegative#✓fully proved

For every natural number \(n\), \(0 \le \binom{2n}{n}/4^n\).

lemma centralBinomialCoeff_nonneg (n : ℕ) : 0 ≤ centralBinomialCoeff n

Uses 1 · Used by 3

Statement usesNormalized central binomial coefficient

Used byTaylor series of the arcsine · Derivative of the integrated arcsine series · Summability of the arcsine series

LemmaNormalized central binomial coefficients are at most one#✓fully proved

For every natural number \(n\), \(\binom{2n}{n}/4^n \le 1\).

lemma centralBinomialCoeff_le_one (n : ℕ) : centralBinomialCoeff n ≤ 1

Uses 1 · Used by 3

Statement usesNormalized central binomial coefficient

Used byTaylor series of the arcsine · Derivative of the integrated arcsine series · Summability of the arcsine series

DefinitionArcsine Taylor series#✓fully proved

Let \(c_n = \binom{2n}{n}/4^n\). For real \(t\), the arcsine Taylor series is

\[S(t) = \sum_{n=0}^{\infty} \frac{c_n\, t^{2n+1}}{2n+1},\]

with the convention that the sum is \(0\) when the series is not summable.

def arcsinSeries (t : ℝ) : ℝ :=
  ∑' n : ℕ, centralBinomialCoeff n * t ^ (2 * n + 1) / ((2 * n + 1 : ℕ) : ℝ)

Uses 1 · Used by 2

Statement usesNormalized central binomial coefficient

Used byTaylor series of the arcsine · Derivative of the integrated arcsine series

DefinitionIntegrated arcsine series#✓fully proved

Let \(c_n = \binom{2n}{n}/4^n\). For real \(t\), the integrated arcsine series is

\[F(t) = \sum_{n=0}^{\infty} \frac{c_n\, t^{2n+1}}{(2n+1)^2},\]

with the convention that the sum is \(0\) when the series is not summable.

Each term is the antiderivative vanishing at \(0\) of the corresponding term \(c_n t^{2n}/(2n+1)\) of \(S(t)/t\), where \(S(t) = \sum_{n \ge 0} c_n t^{2n+1}/(2n+1)\) is the arcsine Taylor series.

def arcsinIntegralSeries (t : ℝ) : ℝ :=
  ∑' n : ℕ, centralBinomialCoeff n * t ^ (2 * n + 1) / ((2 * n + 1 : ℕ) : ℝ) ^ 2

Uses 1 · Used by 5

Statement usesNormalized central binomial coefficient

Used byThe integrated arcsine series vanishes at the origin · Continuity of the integrated arcsine series · Derivative of the integrated arcsine series · The central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

TheoremTaylor series of the arcsine#✓fully proved

For every real \(t\) with \(|t| < 1\),

\[\arcsin t = \sum_{n=0}^{\infty} \frac{\binom{2n}{n}}{4^n} \cdot \frac{t^{2n+1}}{2n+1}.\]

theorem arcsinSeries_eq_arcsin :
    Set.EqOn arcsinSeries Real.arcsin (Set.Ioo (-1 : ℝ) 1)

Uses 4 · Used by 1

Statement usesArcsine Taylor series

Proof usesNormalized central binomial coefficient · Normalized central binomial coefficients are at most one · Normalized central binomial coefficients are nonnegative

Used byDerivative of the integrated arcsine series

LemmaTerms of the integrated arcsine series#✓fully proved

Let \(c_n = \binom{2n}{n}/4^n\) be the normalized central binomial coefficient. For every natural number \(n\) and every real \(t\),

\[\frac{c_n\, t^{2n+1}}{(2n+1)^2} = \frac{\binom{2n}{n}\, t^{2n+1}}{2^{2n}\,(2n+1)^2}.\]

lemma arcsinIntegralSeries_term_eq (n : ℕ) (t : ℝ) :
    centralBinomialCoeff n * t ^ (2 * n + 1) / ((2 * n + 1 : ℕ) : ℝ) ^ 2
      = (Nat.choose (2 * n) n : ℝ) * t ^ (2 * n + 1) /
        ((2 : ℝ) ^ (2 * n) * ((((2 * n + 1 : ℕ)) : ℝ) ^ 2))

Uses 1 · Used by 3

Statement usesNormalized central binomial coefficient

Used byBound on the terms of the integrated arcsine series · The central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

LemmaBound on the terms of the integrated arcsine series#✓fully proved

Write \(c_k = \binom{2k}{k}/4^k\) for the normalized central binomial coefficient. For every real number \(t\) with \(|t| \le 1\) and every natural number \(k\), \(\left|\frac{c_k\, t^{2k+1}}{(2k+1)^2}\right| \le \frac{1}{(k+1)^2}\).

lemma norm_arcsinIntegralSeries_term_le (t : ℝ) (ht : ‖t‖ ≤ 1) (k : ℕ) :
    ‖centralBinomialCoeff k * t ^ (2 * k + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 2‖ ≤
      (1 : ℝ) / (((k : ℝ) + 1) ^ 2)

Uses 2 · Used by 3

Statement usesNormalized central binomial coefficient

Proof usesTerms of the integrated arcsine series

Used byContinuity of the integrated arcsine series · Derivative of the integrated arcsine series · Summability of the integrated arcsine series

TheoremSummability of the integrated arcsine series#✓fully proved

Write \(c_n = \binom{2n}{n}/4^n\) for the normalized central binomial coefficient. For every real number \(t\) with \(|t| \le 1\), the series \(\sum_{n=0}^{\infty} \frac{c_n\, t^{2n+1}}{(2n+1)^2}\) converges absolutely.

theorem summable_arcsinIntegralSeries_term (t : ℝ) (ht : ‖t‖ ≤ 1) :
    Summable (fun n : ℕ =>
      centralBinomialCoeff n * t ^ (2 * n + 1) / ((2 * n + 1 : ℕ) : ℝ) ^ 2)

Uses 2 · Used by 2

Statement usesNormalized central binomial coefficient

Proof usesBound on the terms of the integrated arcsine series

Used byThe central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

TheoremThe integrated arcsine series vanishes at the origin#✓fully proved

The integrated arcsine series \(F(t) = \sum_{n \ge 0} \binom{2n}{n} 4^{-n}\, t^{2n+1}/(2n+1)^2\) satisfies \(F(0) = 0\).

@[simp] theorem arcsinIntegralSeries_zero : arcsinIntegralSeries 0 = 0

Uses 2 · Used by 2

Statement usesIntegrated arcsine series

Proof usesNormalized central binomial coefficient

Used byThe central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

TheoremContinuity of the integrated arcsine series#✓fully proved

The integrated arcsine series \(F(t) = \sum_{n \ge 0} \binom{2n}{n} 4^{-n}\, t^{2n+1}/(2n+1)^2\) is continuous on the closed interval \([-1, 1]\).

theorem continuousOn_arcsinIntegralSeries :
    ContinuousOn arcsinIntegralSeries (Set.Icc (-1 : ℝ) 1)

Uses 3 · Used by 2

Statement usesIntegrated arcsine series

Proof usesNormalized central binomial coefficient · Bound on the terms of the integrated arcsine series

Used byThe central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

TheoremSummability of the arcsine series#✓fully proved

Write \(c_n = \binom{2n}{n}/4^n\) for the normalized central binomial coefficient. For every real number \(y\) with \(|y| < 1\), the series \(\sum_{n=0}^{\infty} \frac{c_n\, y^{2n+1}}{2n+1}\) converges absolutely.

theorem summable_arcsinSeries_term {y : ℝ} (hy : ‖y‖ < 1) :
    Summable (fun n : ℕ => centralBinomialCoeff n * y ^ (2 * n + 1) / ((2 * n + 1 : ℕ) : ℝ))

Uses 3 · Used by 1

Statement usesNormalized central binomial coefficient

Proof usesNormalized central binomial coefficients are at most one · Normalized central binomial coefficients are nonnegative

Used byDerivative of the integrated arcsine series

TheoremDerivative of the integrated arcsine series#✓fully proved

Let \(F(t) = \sum_{n \ge 0} \binom{2n}{n} 4^{-n}\, t^{2n+1}/(2n+1)^2\) be the integrated arcsine series. For every real \(y\) with \(|y| < 1\) and \(y \neq 0\), \(F\) is differentiable at \(y\) with \(F'(y) = \arcsin(y)/y\).

theorem hasDerivAt_arcsinIntegralSeries {y : ℝ} (hy : ‖y‖ < 1) (hy0 : y ≠ 0) :
    HasDerivAt arcsinIntegralSeries (Real.arcsin y / y) y

Uses 8 · Used by 2

Statement usesIntegrated arcsine series

Proof usesArcsine Taylor series · Taylor series of the arcsine · Normalized central binomial coefficient · Normalized central binomial coefficients are at most one · Normalized central binomial coefficients are nonnegative · Bound on the terms of the integrated arcsine series · Summability of the arcsine series

Used byThe central binomial series in \(\cos x\) minus that in \(\sin x\) · Entry 22 of Chapter 9 of Ramanujan's notebooks

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.