Series transformations via Taylor shifts

TheoremRamanujan's binomial series transformation without the radius hypothesis#✓fully proved

Let \(n\) and \(x\) be complex numbers with \(|x| < 1\), write \((n)_k = n(n-1)\cdots(n-k+1)\) for the falling factorial (with \((n)_0 = 1\)), and let \(Q_0, Q_1, Q_2, \ldots\) be complex numbers such that the double series

\[\sum_{j, m \ge 0} \frac{Q_j\, (n)_{j+m}\, x^{j+m}}{m!}\]

is absolutely summable. Then the series

\[\sum_{k=0}^{\infty} \Bigl(\sum_{j=0}^{k} \frac{Q_j}{(k-j)!}\Bigr) (n)_k\, x^k\]

and

\[\sum_{k=0}^{\infty} Q_k\, (n)_k\, x^k\, (1 + x)^{n-k}\]

converge unconditionally to the same sum, where \((1 + x)^{n-k} = e^{(n-k) \log(1+x)}\) with the principal branch of the logarithm.

theorem ramanujan_part1_ch3_entry1_corollary1_binomial_series_general (n x : ℂ)
    (Q : ℕ → ℂ)
        (hx : ‖x‖ < 1)
                (hsum : Summable (fun p : ℕ × ℕ => Q p.1 *
                    (∏ j ∈ Finset.range (p.1 + p.2), (n - (j : ℂ))) * x ^ (p.1 + p.2) /
                        (Nat.factorial p.2 : ℂ))) :
    ∃ s : ℂ,
        HasSum (fun k : ℕ => (∑ j ∈ Finset.range (k + 1), Q j / (Nat.factorial (k - j) : ℂ)) *
            (∏ j ∈ Finset.range k, (n - (j : ℂ))) * x ^ k) s ∧
            HasSum (fun k : ℕ => Q k * (∏ j ∈ Finset.range k, (n - (j : ℂ))) * x ^ k *
                Complex.exp ((n - (k : ℂ)) * Complex.log (1 + x))) s
Used by 1
Used byRamanujan's binomial series transformation (Chapter 3, Entry 1, Corollary 1)

TheoremRamanujan's binomial series transformation (Chapter 3, Entry 1, Corollary 1)#✓fully proved

Let \(n\) and \(x\) be complex numbers with \(|x| < 1\), write \((n)_k = n(n-1)\cdots(n-k+1)\) for the falling factorial (with \((n)_0 = 1\)), and let \(Q_0, Q_1, Q_2, \ldots\) be complex numbers such that, for some \(R > 0\), the power series \(\sum_k Q_k z^k\) converges absolutely for every complex \(z\) with \(|z| < R\). Suppose that the double series

\[\sum_{j, m \ge 0} \frac{Q_j\, (n)_{j+m}\, x^{j+m}}{m!}\]

is absolutely summable. Then the series

\[\sum_{k=0}^{\infty} \Bigl(\sum_{j=0}^{k} \frac{Q_j}{(k-j)!}\Bigr) (n)_k\, x^k\]

and

\[\sum_{k=0}^{\infty} Q_k\, (n)_k\, x^k\, (1 + x)^{n-k}\]

converge unconditionally to the same sum, where \((1 + x)^{n-k} = e^{(n-k) \log(1+x)}\) with the principal branch of the logarithm.

theorem ramanujan_part1_ch3_entry1_corollary1_binomial_series (n x : ℂ)
    (Q : ℕ → ℂ)
        (hx : ‖x‖ < 1)
            (hQ : ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, ‖z‖ < R → Summable (fun k : ℕ => Q k * z ^ k))
                (hsum : Summable (fun p : ℕ × ℕ => Q p.1 *
                    (∏ j ∈ Finset.range (p.1 + p.2), (n - (j : ℂ))) * x ^ (p.1 + p.2) /
                        (Nat.factorial p.2 : ℂ))) :
    ∃ s : ℂ,
        HasSum (fun k : ℕ => (∑ j ∈ Finset.range (k + 1), Q j / (Nat.factorial (k - j) : ℂ)) *
            (∏ j ∈ Finset.range k, (n - (j : ℂ))) * x ^ k) s ∧
            HasSum (fun k : ℕ => Q k * (∏ j ∈ Finset.range k, (n - (j : ℂ))) * x ^ k *
                Complex.exp ((n - (k : ℂ)) * Complex.log (1 + x))) s
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 1, Corollary 1, printed p. 45 / PDF p. 55.
Uses 1
Proof usesRamanujan's binomial series transformation without the radius hypothesis

TheoremRamanujan's series transformation without the radius hypothesis#✓fully proved

Let \(R_1 > 1\), let \(f : \mathbb{C} \to \mathbb{C}\) be analytic on the open disc \(|z| < R_1\), and let \(Q_0, Q_1, Q_2, \ldots\) be complex numbers such that the double series

\[\sum_{j, m \ge 0} \frac{Q_j\, f^{(j+m)}(0)}{m!}\]

is absolutely summable. Then the series

\[\sum_{n=0}^{\infty} \Bigl(\sum_{j=0}^{n} \frac{Q_j}{(n-j)!}\Bigr) f^{(n)}(0)\]

and

\[\sum_{n=0}^{\infty} Q_n\, f^{(n)}(1)\]

converge unconditionally to the same sum.

theorem ramanujan_part1_ch3_entry1_series_transformation_general
    (R₁ : ℝ) (hR₁ : 1 < R₁)
    (f : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.ball (0 : ℂ) R₁))
    (Q : ℕ → ℂ)
    (hSumm : Summable (fun p : ℕ × ℕ => Q p.1 * iteratedDeriv (p.1 + p.2) f (0 : ℂ) /
        ((Nat.factorial p.2 : ℂ)))) :
    ∃ v : ℂ,
        HasSum (fun n : ℕ => (∑ j ∈ Finset.range (n + 1), Q j / ((Nat.factorial (n - j) : ℂ))) *
            iteratedDeriv n f (0 : ℂ)) v ∧
            HasSum (fun n : ℕ => Q n * iteratedDeriv n f (1 : ℂ)) v
Used by 1
Used byRamanujan's series transformation (Chapter 3, Entry 1)

TheoremRamanujan's series transformation (Chapter 3, Entry 1)#✓fully proved

Let \(R_1 > 1\), let \(f : \mathbb{C} \to \mathbb{C}\) be analytic on the open disc \(|z| < R_1\), and let \(Q_0, Q_1, Q_2, \ldots\) be complex numbers such that, for some \(R_2 > 0\), the power series \(\sum_n Q_n z^n\) converges absolutely for every complex \(z\) with \(|z| < R_2\). Suppose that the double series

\[\sum_{j, m \ge 0} \frac{Q_j\, f^{(j+m)}(0)}{m!}\]

is absolutely summable. Then the series

\[\sum_{n=0}^{\infty} \Bigl(\sum_{j=0}^{n} \frac{Q_j}{(n-j)!}\Bigr) f^{(n)}(0)\]

and

\[\sum_{n=0}^{\infty} Q_n\, f^{(n)}(1)\]

converge unconditionally to the same sum.

theorem ramanujan_part1_ch3_entry1_series_transformation
    (R₁ : ℝ) (hR₁ : 1 < R₁)
    (f : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.ball (0 : ℂ) R₁))
    (Q : ℕ → ℂ)
    (hQ : ∃ R₂ : ℝ, 0 < R₂ ∧ ∀ z : ℂ, ‖z‖ < R₂ → Summable (fun n : ℕ => Q n * z ^ n))
    (hSumm : Summable (fun p : ℕ × ℕ => Q p.1 * iteratedDeriv (p.1 + p.2) f (0 : ℂ) /
        ((Nat.factorial p.2 : ℂ)))) :
    ∃ v : ℂ,
        HasSum (fun n : ℕ => (∑ j ∈ Finset.range (n + 1), Q j / ((Nat.factorial (n - j) : ℂ))) *
            iteratedDeriv n f (0 : ℂ)) v ∧
            HasSum (fun n : ℕ => Q n * iteratedDeriv n f (1 : ℂ)) v
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 1, printed p. 45 / PDF p. 55.
Uses 1
Proof usesRamanujan's series transformation without the radius hypothesis
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.