Partial-fraction series over odd integers
TheoremDifference series over \(2k+1 \pm a\) that are polynomials on \((-\pi, \pi)\)#✓fully proved
Let \(r\) be a positive integer, \(a\) a real number that is not an odd integer, and \(x\) a real number with \(|x| < \pi\). For a natural number \(s\) let \(c_k(s) = (2k+1-a)^{-s} - (2k+1+a)^{-s}\) and \(C_s(a) = \sum_{k=0}^{\infty} c_k(s)\). Then \(\sum_k c_k(r)\) is summable, and either \(r\) is odd, \(\sum_k c_k(r-2j)\) is summable for \(0 \le j \le (r-1)/2\), and the partial sums of \(\sum_{k=0}^{\infty} \bigl(\frac{\cos((2k+1-a)x)}{(2k+1-a)^r} - \frac{\cos((2k+1+a)x)}{(2k+1+a)^r}\bigr)\) converge to \(\sum_{j=0}^{(r-1)/2} (-1)^j C_{r-2j}(a) \frac{x^{2j}}{(2j)!}\); or \(r\) is even, \(\sum_k c_k(r-2j-1)\) is summable for \(0 \le j < r/2\), and the partial sums of \(\sum_{k=0}^{\infty} \bigl(\frac{\sin((2k+1-a)x)}{(2k+1-a)^r} - \frac{\sin((2k+1+a)x)}{(2k+1+a)^r}\bigr)\) converge to \(\sum_{0 \le j < r/2} (-1)^j C_{r-2j-1}(a) \frac{x^{2j+1}}{(2j+1)!}\).
MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry1Logratio.ramanujan_part1_ch9_entry1_logratio · 25 lines
theorem ramanujan_part1_ch9_entry1_logratio (r : ℕ) (a x : ℝ)
(hr : 0 < r)
(ha : ∀ z : ℤ, a ≠ ((2 * z + 1 : ℤ) : ℝ))
(hx : |x| < Real.pi) :
Summable (chapter9Entry1ConstantTerm r a) ∧
((Odd r ∧
(∀ k ∈ range ((r - 1) / 2 + 1),
Summable (chapter9Entry1ConstantTerm (r - 2 * k) a)) ∧
Tendsto
(fun N : ℕ =>
∑ k ∈ range N, chapter9Entry1CosineTerm r a x k)
atTop
(𝓝 (∑ k ∈ range ((r - 1) / 2 + 1),
(-1 : ℝ) ^ k * chapter9Entry1Constant (r - 2 * k) a *
x ^ (2 * k) / ((2 * k).factorial : ℝ)))) ∨
(Even r ∧
(∀ k ∈ range (r / 2),
Summable (chapter9Entry1ConstantTerm (r - 2 * k - 1) a)) ∧
Tendsto
(fun N : ℕ =>
∑ k ∈ range N, chapter9Entry1SineTerm r a x k)
atTop
(𝓝 (∑ k ∈ range (r / 2),
(-1 : ℝ) ^ k * chapter9Entry1Constant (r - 2 * k - 1) a *
x ^ (2 * k + 1) / ((2 * k + 1).factorial : ℝ)))))def chapter9Entry1ConstantTerm (r : ℕ) (a : ℝ) (k : ℕ) : ℝ :=
1 / ((((2 * k + 1 : ℕ) : ℝ) - a) ^ r) -
1 / ((((2 * k + 1 : ℕ) : ℝ) + a) ^ r)MathlibExt/Analysis/Ramanujan/Part1Ch9Entry1Logratio.lean:50
def chapter9Entry1CosineTerm (r : ℕ) (a x : ℝ) (k : ℕ) : ℝ :=
Real.cos (((((2 * k + 1 : ℕ) : ℝ) - a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) - a) ^ r) -
Real.cos (((((2 * k + 1 : ℕ) : ℝ) + a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) + a) ^ r)MathlibExt/Analysis/Ramanujan/Part1Ch9Entry1Logratio.lean:57
def chapter9Entry1Constant (r : ℕ) (a : ℝ) : ℝ :=
∑' k : ℕ, chapter9Entry1ConstantTerm r a kMathlibExt/Analysis/Ramanujan/Part1Ch9Entry1Logratio.lean:54
def chapter9Entry1SineTerm (r : ℕ) (a x : ℝ) (k : ℕ) : ℝ :=
Real.sin (((((2 * k + 1 : ℕ) : ℝ) - a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) - a) ^ r) -
Real.sin (((((2 * k + 1 : ℕ) : ℝ) + a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) + a) ^ r)MathlibExt/Analysis/Ramanujan/Part1Ch9Entry1Logratio.lean:63
Sources
- Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9, Entry 1, pp. 233–235.
TheoremSum series over \(2k+1 \pm a\) on \((0, \pi)\)#✓fully proved
Let \(r \ge 2\) be an integer, \(a\) a real number that is not an odd integer, and \(x\) a real number with \(0 < x < \pi\). For a natural number \(s\) let \(d_k(s) = (2k+1-a)^{-s} + (2k+1+a)^{-s}\) and \(D_s(a) = \sum_{k=0}^{\infty} d_k(s)\). Then \(\sum_k d_k(r)\) is summable, and either \(r\) is even, \(\sum_k d_k(r-2j)\) is summable for \(0 \le j < r/2\), and the partial sums of \(\sum_{k=0}^{\infty} \bigl(\frac{\cos((2k+1-a)x)}{(2k+1-a)^r} + \frac{\cos((2k+1+a)x)}{(2k+1+a)^r}\bigr)\) converge to \(\sum_{0 \le j < r/2} (-1)^j D_{r-2j}(a) \frac{x^{2j}}{(2j)!} + (-1)^{r/2} \frac{\pi x^{r-1}}{2 (r-1)!}\); or \(r\) is odd, \(\sum_k d_k(r-1-2j)\) is summable for \(0 \le j < (r-1)/2\), and the partial sums of \(\sum_{k=0}^{\infty} \bigl(\frac{\sin((2k+1-a)x)}{(2k+1-a)^r} + \frac{\sin((2k+1+a)x)}{(2k+1+a)^r}\bigr)\) converge to \(\sum_{0 \le j < (r-1)/2} (-1)^j D_{r-1-2j}(a) \frac{x^{2j+1}}{(2j+1)!} + (-1)^{(r-1)/2} \frac{\pi x^{r-1}}{2 (r-1)!}\).
MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry2.ramanujan_part1_ch9_entry2 · 29 lines
theorem ramanujan_part1_ch9_entry2 (r : ℕ) (a x : ℝ)
(hr : 2 ≤ r)
(ha : ∀ z : ℤ, a ≠ ((2 * z + 1 : ℤ) : ℝ))
(hxLower : 0 < x) (hxUpper : x < Real.pi) :
Summable (chapter9Entry2ConstantTerm r a) ∧
((Even r ∧
(∀ k ∈ range (r / 2),
Summable (chapter9Entry2ConstantTerm (r - 2 * k) a)) ∧
Tendsto
(fun N : ℕ =>
∑ k ∈ range N, chapter9Entry2CosineTerm r a x k)
atTop
(𝓝 ((∑ k ∈ range (r / 2),
(-1 : ℝ) ^ k * chapter9Entry2Constant (r - 2 * k) a *
x ^ (2 * k) / ((2 * k).factorial : ℝ)) +
(-1 : ℝ) ^ (r / 2) * Real.pi * x ^ (r - 1) /
(2 * ((r - 1).factorial : ℝ))))) ∨
(Odd r ∧
(∀ k ∈ range ((r - 1) / 2),
Summable (chapter9Entry2ConstantTerm (r - 1 - 2 * k) a)) ∧
Tendsto
(fun N : ℕ =>
∑ k ∈ range N, chapter9Entry2SineTerm r a x k)
atTop
(𝓝 ((∑ k ∈ range ((r - 1) / 2),
(-1 : ℝ) ^ k * chapter9Entry2Constant (r - 1 - 2 * k) a *
x ^ (2 * k + 1) / ((2 * k + 1).factorial : ℝ)) +
(-1 : ℝ) ^ ((r - 1) / 2) * Real.pi * x ^ (r - 1) /
(2 * ((r - 1).factorial : ℝ))))))def chapter9Entry2ConstantTerm (r : ℕ) (a : ℝ) (k : ℕ) : ℝ :=
1 / ((((2 * k + 1 : ℕ) : ℝ) - a) ^ r) +
1 / ((((2 * k + 1 : ℕ) : ℝ) + a) ^ r)MathlibExt/Analysis/Ramanujan/Part1Ch9Entry2.lean:67
def chapter9Entry2CosineTerm (r : ℕ) (a x : ℝ) (k : ℕ) : ℝ :=
Real.cos (((((2 * k + 1 : ℕ) : ℝ) - a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) - a) ^ r) +
Real.cos (((((2 * k + 1 : ℕ) : ℝ) + a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) + a) ^ r)MathlibExt/Analysis/Ramanujan/Part1Ch9Entry2.lean:74
def chapter9Entry2Constant (r : ℕ) (a : ℝ) : ℝ :=
∑' k : ℕ, chapter9Entry2ConstantTerm r a kMathlibExt/Analysis/Ramanujan/Part1Ch9Entry2.lean:71
def chapter9Entry2SineTerm (r : ℕ) (a x : ℝ) (k : ℕ) : ℝ :=
Real.sin (((((2 * k + 1 : ℕ) : ℝ) - a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) - a) ^ r) +
Real.sin (((((2 * k + 1 : ℕ) : ℝ) + a) * x)) /
((((2 * k + 1 : ℕ) : ℝ) + a) ^ r)MathlibExt/Analysis/Ramanujan/Part1Ch9Entry2.lean:80
Sources
- Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.