Transformations of factorial series
TheoremTwo derivative series with the same sum (Chapter 3, Entry 2, Corollary 1)#✓fully proved
Let \(R > 1\), let \(f : \mathbb{C} \to \mathbb{C}\) be analytic on the open disc \(|w| < R\), and let \(z\) be a complex number with \(z + n \ne 0\) for every natural number \(n\). Suppose that the double series \(\sum_{j, m \ge 0} \frac{(-1)^j}{z(z+1)\cdots(z+j)} \cdot \frac{f^{(j+m)}(0)}{m!}\) converges absolutely. Then there is a complex number \(c\) such that the series \(\sum_{k \ge 0} \frac{f^{(k)}(0)}{(z+k)\, k!}\) and \(\sum_{k \ge 0} \frac{(-1)^k f^{(k)}(1)}{z(z+1)\cdots(z+k)}\) both converge absolutely with sum \(c\).
theorem ramanujan_part1_ch3_entry2_corollary1_derivative_series (R : ℝ)
(hR : 1 < R)
(f : ℂ → ℂ)
(hf : AnalyticOn ℂ f (Metric.ball (0 : ℂ) R))
(z : ℂ)
(hz : ∀ n : ℕ, z + (n : ℂ) ≠ 0)
(hSumm : Summable (fun p : ℕ × ℕ => (-1 : ℂ) ^ p.1 /
(Finset.range (p.1 + 1)).prod (fun i => z + (i : ℂ)) *
(iteratedDeriv (p.1 + p.2) f (0 : ℂ) / (Nat.factorial p.2 : ℂ)))) :
∃ c : ℂ,
HasSum (fun k : ℕ => iteratedDeriv k f (0 : ℂ) /
((z + (k : ℂ)) * (Nat.factorial k : ℂ))) c ∧
HasSum (fun k : ℕ => (-1 : ℂ) ^ k * iteratedDeriv k f (1 : ℂ) /
(Finset.range (k + 1)).prod (fun i => z + (i : ℂ))) cSources
- Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 2, Corollary 1, printed p. 46 / PDF p. 56.
TheoremAgreement of two definitions of the harmonic numbers#✓fully proved
For every natural number \(n\), the rational number \(\sum_{k=0}^{n-1} \frac{1}{k+1}\) equals Mathlib's harmonic number \(H_n = \sum_{k=0}^{n-1} (k+1)^{-1}\).
theorem harmonic_eq_mathlib_harmonic (n : ℕ) :
harmonic n = _root_.harmonic ndef harmonic (n : ℕ) : ℚ :=
(Finset.range n).sum fun k => (1 : ℚ) / ((k + 1 : ℕ) : ℚ)MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry2Corollary2HarmonicSeries.lean:50
TheoremRamanujan's series for the harmonic numbers, with Mathlib's harmonic numbers#✓fully proved
Let \(H_k = \sum_{i=0}^{k-1} (i+1)^{-1}\) be Mathlib's \(k\)-th harmonic number. For every complex number \(x\), the series \(\sum_{k \ge 1} \frac{H_k x^k}{k!}\) and \(\sum_{k \ge 1} \frac{(-1)^{k-1} x^k}{k!\, k}\) converge absolutely, and \(\sum_{k=1}^{\infty} \frac{H_k x^k}{k!} = e^x \sum_{k=1}^{\infty} \frac{(-1)^{k-1} x^k}{k!\, k}\).
theorem ramanujan_part1_ch3_entry2_corollary2_harmonic_series_mathlib (x : ℂ) :
Summable (fun j : ℕ => (_root_.harmonic (j + 1) : ℂ) * x ^ (j + 1) /
(Nat.factorial (j + 1) : ℂ)) ∧
Summable (fun j : ℕ =>
((-1 : ℂ) ^ j * x ^ (j + 1) / ((Nat.factorial (j + 1) : ℂ) * ((j + 1 : ℕ) : ℂ)))) ∧
(∑' j : ℕ, (_root_.harmonic (j + 1) : ℂ) * x ^ (j + 1) / (Nat.factorial (j + 1) : ℂ)) =
Complex.exp x *
(∑' j : ℕ,
((-1 : ℂ) ^ j * x ^ (j + 1) / ((Nat.factorial (j + 1) : ℂ) *
((j + 1 : ℕ) : ℂ))))TheoremRamanujan's series for the harmonic numbers (Chapter 3, Entry 2, Corollary 2)#✓fully proved
Let \(H_k = \sum_{i=1}^{k} \frac{1}{i}\) be the \(k\)-th harmonic number. For every complex number \(x\), the series \(\sum_{k \ge 1} \frac{H_k x^k}{k!}\) and \(\sum_{k \ge 1} \frac{(-1)^{k-1} x^k}{k!\, k}\) converge absolutely, and \(\sum_{k=1}^{\infty} \frac{H_k x^k}{k!} = e^x \sum_{k=1}^{\infty} \frac{(-1)^{k-1} x^k}{k!\, k}\).
theorem ramanujan_part1_ch3_entry2_corollary2_harmonic_series (x : ℂ) :
Summable (fun j : ℕ => (harmonic (j + 1) : ℂ) * x ^ (j + 1) / (Nat.factorial (j + 1) : ℂ)) ∧
Summable (fun j : ℕ =>
((-1 : ℂ) ^ j * x ^ (j + 1) / ((Nat.factorial (j + 1) : ℂ) * ((j + 1 : ℕ) : ℂ)))) ∧
(∑' j : ℕ, (harmonic (j + 1) : ℂ) * x ^ (j + 1) / (Nat.factorial (j + 1) : ℂ)) =
Complex.exp x *
(∑' j : ℕ,
((-1 : ℂ) ^ j * x ^ (j + 1) / ((Nat.factorial (j + 1) : ℂ) *
((j + 1 : ℕ) : ℂ))))def harmonic (n : ℕ) : ℚ :=
(Finset.range n).sum fun k => (1 : ℚ) / ((k + 1 : ℕ) : ℚ)MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry2Corollary2HarmonicSeries.lean:50
Sources
- Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 2, formula (2.3) and Corollary 2, printed pp. 46--47 / PDF pp. 56--57.
TheoremConvergence of the right side of Ramanujan's Chapter 3, Entry 2#✓fully proved
For all complex numbers \(x\) and \(z\) such that \(z + r \ne 0\) for every natural number \(r\), the series \(\sum_{j \ge 0} \frac{(-1)^j x^{j+1}}{z(z+1)\cdots(z+j)}\) converges absolutely.
theorem ramanujan_part1_ch3_entry2_rightsummable (x z : ℂ) (hz : ∀ r : ℕ, z + (r : ℂ) ≠ 0) :
Summable (fun j : ℕ =>
((-1 : ℂ) ^ j * x ^ (j + 1) / (∏ k ∈ Finset.range (j + 1), (z + (k : ℂ)))))Sources
- Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 2, formula (2.1), printed p. 46 / PDF p. 56.
TheoremRamanujan's exponential transformation of a factorial series (Chapter 3, Entry 2)#✓fully proved
For all complex numbers \(x\) and \(z\) such that \(z + r \ne 0\) for every natural number \(r\), the series \(\sum_{j \ge 0} \frac{x^{j+1}}{(z+j)\, j!}\) converges absolutely, and its sum is \(e^x \sum_{j \ge 0} \frac{(-1)^j x^{j+1}}{z(z+1)\cdots(z+j)}\).
theorem ramanujan_part1_ch3_entry2 (x z : ℂ) (hz : ∀ r : ℕ, (z + (r : ℂ)) ≠ 0) :
HasSum (fun j : ℕ => x ^ (j + 1) / ((z + (j : ℂ)) * (Nat.factorial j : ℂ)))
(Complex.exp x * ∑' (j : ℕ),
((-1 : ℂ) ^ j * x ^ (j + 1) / ∏ k ∈ Finset.range (j + 1), (z + (k : ℂ))))Sources
- Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 2, formula (2.1), printed p. 46 / PDF p. 56.
TheoremConvergence of the left side of Ramanujan's Chapter 3, Entry 2#✓fully proved
For all complex numbers \(x\) and \(z\) such that \(z + r \ne 0\) for every natural number \(r\), the series \(\sum_{j \ge 0} \frac{x^{j+1}}{(z+j)\, j!}\) converges absolutely.
theorem ramanujan_part1_ch3_entry2_leftsummable (x z : ℂ) (hz : ∀ r : ℕ, z + (r : ℂ) ≠ 0) :
Summable (fun j : ℕ => x ^ (j + 1) / ((z + (j : ℂ)) * (Nat.factorial j : ℂ)))Sources
- Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 2, formula (2.1), printed p. 46 / PDF p. 56.
TheoremRamanujan's companion series transformation (Chapter 3, Entry 2, formula (2.3))#✓fully proved
Let \(x\) and \(z\) be complex numbers with \(z \ne -(n+1)\) for every natural number \(n\). Then the series \(\sum_{j \ge 0} \frac{(-1)^j x^{j+1}}{(z+j+1)\, j!}\) converges absolutely, say with sum \(S\), and the series \(\sum_{j \ge 0} \frac{x^{j+1}}{(z+1)(z+2)\cdots(z+j+1)}\) converges absolutely with sum \(e^x S\).
The identity follows from Entry 2 applied with \(-x\) and \(z + 1\) in place of \(x\) and \(z\), using \(e^x e^{-x} = 1\).
theorem ramanujan_part1_ch3_entry2_formula23_series_pair
(x z : ℂ) (hz : ∀ n : ℕ, z ≠ -((n : ℂ) + 1)) :
HasSum (fun j : ℕ => (x ^ (j + 1) / ∏ i ∈ Finset.range (j + 1), (z + ((i : ℂ) + 1)),
(-1 : ℂ) ^ j * x ^ (j + 1) / ((z + ((j : ℂ) + 1)) * ((Nat.factorial j : ℕ) : ℂ))))
(Complex.exp x * ∑' j : ℕ,
((-1 : ℂ) ^ j * x ^ (j + 1) / ((z + ((j : ℂ) + 1)) * ((Nat.factorial j : ℕ) : ℂ))),
∑' j : ℕ, ((-1 : ℂ) ^ j * x ^ (j + 1) / ((z + ((j : ℂ) + 1)) * ((Nat.factorial j : ℕ) : ℂ))))Sources
- Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 2, formula (2.3) and Corollary 2, printed pp. 46--47 / PDF pp. 56--57.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.