Series of the form Σ rᵏ/(1 − a xᵏ)

TheoremRamanujan's transformation of the alternating series of 1/(x^k - 1)#✓fully proved

For every real number \(x\) with \(|x| > 1\), we have \(x^k - 1 \ne 0\) and \(x^{k^2}(x^{2k} - 1) \ne 0\) for every integer \(k \ge 1\), the series \(\sum_{k \ge 1} (-1)^{k+1}/(x^k - 1)\) and \(\sum_{k \ge 1} (-1)^{k+1}(x^{2k} + 1)/(x^{k^2}(x^{2k} - 1))\) are summable, and \(\sum_{k=1}^{\infty} (-1)^{k+1}/(x^k - 1) = \sum_{k=1}^{\infty} (-1)^{k+1}(x^{2k} + 1)/(x^{k^2}(x^{2k} - 1))\).

theorem ramanujan_part1_ch6_entry13_ramanujanfactorial (x : ℝ) (hx : 1 < |x|) :
    let leftTerm := fun j : ℕ =>
      (-1 : ℝ) ^ (j + 2) / (x ^ (j + 1) - 1)
    let rightTerm := fun j : ℕ =>
      ((-1 : ℝ) ^ (j + 2) * (x ^ (2 * (j + 1)) + 1)) /
        (x ^ ((j + 1) ^ 2) * (x ^ (2 * (j + 1)) - 1))
    (∀ j : ℕ, x ^ (j + 1) - 1 ≠ 0) ∧
      (∀ j : ℕ,
        x ^ ((j + 1) ^ 2) * (x ^ (2 * (j + 1)) - 1) ≠ 0) ∧
      Summable leftTerm ∧ Summable rightTerm ∧
      ∑' j, leftTerm j = ∑' j, rightTerm j

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 6.

TheoremA finite identity for \(\sum_k r^k/(1-ax^k)\) over a field#✓fully proved

Let \(K\) be a field, let \(a, r, x \in K\) and let \(n \ge 0\) be an integer. Suppose that \(1 - a x^k \ne 0\) and \(1 - r x^{k-1} \ne 0\) for every integer \(k\) with \(1 \le k \le n\). Then \(\sum_{k=1}^{n} \frac{r^k}{1 - a x^k} = \sum_{k=1}^{n} \frac{(a r x^k)^k}{1 - a x^k} + \sum_{k=1}^{n} \frac{a^{k-1} \left( (r x^{k-1})^k - (r x^{k-1})^{n+1} \right)}{1 - r x^{k-1}}\). For \(n = 0\) all three sums are empty.

theorem ramanujan_part1_ch6_entry16_finite_sum_general
    {K : Type*} [Field K] (a r x : K) (n : ℕ)
    (hax : ∀ k ∈ Icc 1 n, 1 - a * x ^ k ≠ 0)
    (hrx : ∀ k ∈ Icc 1 n, 1 - r * x ^ (k - 1) ≠ 0) :
    ∑ k ∈ Icc 1 n, r ^ k / (1 - a * x ^ k) =
      (∑ k ∈ Icc 1 n,
        (a * r * x ^ k) ^ k / (1 - a * x ^ k)) +
      ∑ k ∈ Icc 1 n,
        a ^ (k - 1) *
          ((r * x ^ (k - 1)) ^ k - (r * x ^ (k - 1)) ^ (n + 1)) /
            (1 - r * x ^ (k - 1))

Used by 1

Used byRamanujan's finite identity for \(\sum_k r^k/(1-ax^k)\)

TheoremRamanujan's finite identity for \(\sum_k r^k/(1-ax^k)\)#✓fully proved

Let \(a, r, x\) be real numbers and let \(n\) be a positive integer. Suppose that \(1 - a x^k \ne 0\) and \(1 - r x^{k-1} \ne 0\) for every integer \(k\) with \(1 \le k \le n\). Then \(\sum_{k=1}^{n} \frac{r^k}{1 - a x^k} = \sum_{k=1}^{n} \frac{(a r x^k)^k}{1 - a x^k} + \sum_{k=1}^{n} \frac{a^{k-1} \left( (r x^{k-1})^k - (r x^{k-1})^{n+1} \right)}{1 - r x^{k-1}}\).

theorem ramanujan_part1_ch6_entry16_finite_sum
    (a r x : ℝ) (n : ℕ) (hn : 0 < n)
    (hax : ∀ k ∈ Icc 1 n, 1 - a * x ^ k ≠ 0)
    (hrx : ∀ k ∈ Icc 1 n, 1 - r * x ^ (k - 1) ≠ 0) :
    ∑ k ∈ Icc 1 n, r ^ k / (1 - a * x ^ k) =
      (∑ k ∈ Icc 1 n,
        (a * r * x ^ k) ^ k / (1 - a * x ^ k)) +
      ∑ k ∈ Icc 1 n,
        a ^ (k - 1) *
          ((r * x ^ (k - 1)) ^ k - (r * x ^ (k - 1)) ^ (n + 1)) /
            (1 - r * x ^ (k - 1))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 6. It follows from ramanujan_part1_ch6_entry16_finite_sum_general with K := ℝ; the hypothesis hn is unused and keeps the source's shape.

Uses 1

Proof usesA finite identity for \(\sum_k r^k/(1-ax^k)\) over a field

TheoremRamanujan's infinite identity for \(\sum_k r^k/(1-ax^k)\)#✓fully proved

Let \(a, r, x\) be complex numbers with \(|r| < 1\) and \(|x| \le 1\) such that \(1 - a x^k \ne 0\) for every integer \(k \ge 1\), and such that, if \(|x| = 1\), then \(|a r| < 1\) and there is a real \(\delta > 0\) with \(|1 - a x^k| \ge \delta\) for every \(k \ge 1\). Then \(1 - r x^{k-1} \ne 0\) for every \(k \ge 1\), the three series \(\sum_{k=1}^{\infty} \frac{r^k}{1 - a x^k}\), \(\sum_{k=1}^{\infty} \frac{(a r x^k)^k}{1 - a x^k}\) and \(\sum_{k=1}^{\infty} \frac{a^{k-1} r^k x^{(k-1)k}}{1 - r x^{k-1}}\) are summable, and the first equals the sum of the other two.

MathlibExt.Analysis.Ramanujan.Part1Ch6.Entry16InfiniteSum.ramanujan_part1_ch6_entry16_infinite_sum · 15 lines

theorem ramanujan_part1_ch6_entry16_infinite_sum
    (a r x : ℂ)
    (hr : ‖r‖ < 1) (hx : ‖x‖ ≤ 1)
    (hboundary : ‖x‖ = 1 → ‖a * r‖ < 1)
    (hpoles : ∀ k : ℕ, 1 ≤ k → 1 - a * x ^ k ≠ 0)
    (hboundarySeparated : ‖x‖ = 1 →
      ∃ delta : ℝ, 0 < delta ∧
        ∀ k : ℕ, 1 ≤ k → delta ≤ ‖1 - a * x ^ k‖) :
    (∀ k : ℕ, 1 ≤ k → 1 - r * x ^ (k - 1) ≠ 0) ∧
      Summable (chapter6Entry16LeftTerm a r x) ∧
      Summable (chapter6Entry16MiddleTerm a r x) ∧
      Summable (chapter6Entry16RightTerm a r x) ∧
      (∑' j : ℕ, chapter6Entry16LeftTerm a r x j) =
        (∑' j : ℕ, chapter6Entry16MiddleTerm a r x j) +
          ∑' j : ℕ, chapter6Entry16RightTerm a r x j

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 6. The infinite form of Entry16FiniteSum.ramanujan_part1_ch6_entry16_finite_sum.

TheoremRamanujan's identity for \(\sum_k (a + kb) \nu^k / (1 - m x^k)\)#✓fully proved

Let \(a, b, m, \nu, x\) be real numbers with \(|x| \le 1\), \(|\nu| < 1\) and \(m \ne 0\), such that \(|m \nu| < 1\) if \(|x| = 1\), and such that \(1 - m x^k \ne 0\) for every integer \(k \ge 0\) (here \(x^0 = 1\)). Then \(1 - \nu x^k \ne 0\) for every \(k \ge 0\), the series \(L = \sum_{k=0}^{\infty} \frac{(a + kb) \, \nu^k}{1 - m x^k}\), \(F = \sum_{k=0}^{\infty} \frac{(a + kb) (1 - m \nu x^{2k}) (m \nu x^k)^k}{(1 - m x^k)(1 - \nu x^k)}\) and \(G = \sum_{k=0}^{\infty} \frac{(m \nu x^k)^{k+1}}{(1 - \nu x^k)^2}\) are summable, and \(L = F + \frac{b}{m} G\).

MathlibExt.Analysis.Ramanujan.Part1Ch6.Entry17Stirlingcoeffs.ramanujan_part1_ch6_entry17_stirlingcoeffs · 18 lines

theorem ramanujan_part1_ch6_entry17_stirlingcoeffs
    (a b m nu x : ℝ)
    (hx : |x| ≤ 1) (hnu : |nu| < 1)
    (hboundary : |x| = 1 → |m * nu| < 1)
    (hm : m ≠ 0)
    (hmx : ∀ k : ℕ, 1 - m * x ^ k ≠ 0) :
    let leftTerm := fun k : ℕ =>
      (a + (k : ℝ) * b) * nu ^ k / (1 - m * x ^ k)
    let firstTerm := fun k : ℕ =>
      ((a + (k : ℝ) * b) * (1 - m * nu * x ^ (2 * k)) *
          (m * nu * x ^ k) ^ k) /
        ((1 - m * x ^ k) * (1 - nu * x ^ k))
    let secondTerm := fun k : ℕ =>
      (m * nu * x ^ k) ^ (k + 1) / (1 - nu * x ^ k) ^ 2
    (∀ k : ℕ, 1 - nu * x ^ k ≠ 0) ∧
      Summable leftTerm ∧ Summable firstTerm ∧ Summable secondTerm ∧
      ∑' k, leftTerm k =
        ∑' k, firstTerm k + b / m * ∑' k, secondTerm k

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 6.

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.