Ramanujan's extension of partial sums

DefinitionTerms of the shifted derivative series#✓fully proved

For \(f : \mathbb{R} \to \mathbb{R}\), natural numbers \(q\) and \(k\), and \(x \in \mathbb{R}\), the \(k\)-th term of the shifted series of \(q\)-th derivatives of \(f\) is \(f^{(q)}(k + 1 + x)\), where \(f^{(q)}\) is the \(q\)-th iterated derivative of \(f\) and a derivative that does not exist is taken to be \(0\).

def chapter6ShiftedDerivedSeriesTerm
    (f : ℝ → ℝ) (q : ℕ) (x : ℝ) (k : ℕ) : ℝ :=
  iteratedDeriv q f ((k : ℝ) + 1 + x)

Used by 9

Used byRamanujan's extension of partial sums · Ramanujan's extension agrees with the partial sums at natural numbers · Difference equation for Ramanujan's extension · Ramanujan's derivative-series constants · Taylor expansion of Ramanujan's extension at the origin · The derivative-series constant is the sum of its series · Derivatives of Ramanujan's extension at the origin · Ramanujan's extension of the partial sums of a smooth function · Tails of the shifted series of derivatives converge

DefinitionRamanujan's derivative-series constants#✓fully proved

For \(f : \mathbb{R} \to \mathbb{R}\) and a natural number \(q\), the constant \(c_q\) is \(\sum_{k \ge 1} f^{(q)}(k)\), the sum of the values of the \(q\)-th iterated derivative of \(f\) at the positive integers, where a derivative that does not exist is taken to be \(0\) and a series that is not summable is given the value \(0\).

def chapter6DerivedSeriesConstant (f : ℝ → ℝ) (q : ℕ) : ℝ :=
  ∑' k : ℕ, chapter6ShiftedDerivedSeriesTerm f q 0 k

Uses 1 · Used by 8

Statement usesTerms of the shifted derivative series

Used byRamanujan's extension of partial sums · Ramanujan's extension agrees with the partial sums at natural numbers · Difference equation for Ramanujan's extension · Terms of the Taylor series in Entry 6 · Taylor expansion of Ramanujan's extension at the origin · The derivative-series constant is the sum of its series · Derivatives of Ramanujan's extension at the origin · Ramanujan's extension of the partial sums of a smooth function

DefinitionRamanujan's extension of partial sums#✓fully proved

For \(f : \mathbb{R} \to \mathbb{R}\), the extension of the partial sums of \(f\) to real arguments is the function \(F(x) = \sum_{k \ge 1} f(k) - \sum_{k \ge 1} f(k + x)\) on \(\mathbb{R}\), where each series is an unconditional sum and a series that is not summable is given the value \(0\).

When \(\sum_{k \ge 1} f(k)\) is summable, \(F(m) = f(1) + \cdots + f(m)\) for every natural number \(m\).

def chapter6ConvergentSumExtension (f : ℝ → ℝ) (x : ℝ) : ℝ :=
  chapter6DerivedSeriesConstant f 0 -
    ∑' k : ℕ, chapter6ShiftedDerivedSeriesTerm f 0 x k

Uses 2 · Used by 5

Statement usesRamanujan's derivative-series constants · Terms of the shifted derivative series

Used byRamanujan's extension agrees with the partial sums at natural numbers · Difference equation for Ramanujan's extension · Taylor expansion of Ramanujan's extension at the origin · Derivatives of Ramanujan's extension at the origin · Ramanujan's extension of the partial sums of a smooth function

DefinitionTerms of the Taylor series in Entry 6#✓fully proved

For \(f : \mathbb{R} \to \mathbb{R}\), \(x \in \mathbb{R}\) and a natural number \(j\), the \(j\)-th term is \(-c_{j+1} x^{j+1} / (j+1)!\), where \(c_q = \sum_{k \ge 1} f^{(q)}(k)\) with \(f^{(q)}\) the \(q\)-th iterated derivative of \(f\); a derivative that does not exist is taken to be \(0\) and a series that is not summable is given the value \(0\).

Under the smoothness, summability and domination hypotheses of Entry 6, these are the nonconstant terms of the Taylor series at \(0\) of Ramanujan's extension \(F(x) = \sum_{k \ge 1} f(k) - \sum_{k \ge 1} f(k + x)\), whose constant term is \(F(0) = 0\).

def chapter6Entry6Term
    (f : ℝ → ℝ) (x : ℝ) (j : ℕ) : ℝ :=
  -chapter6DerivedSeriesConstant f (j + 1) * x ^ (j + 1) /
    ((j + 1).factorial : ℝ)

Uses 1 · Used by 2

Statement usesRamanujan's derivative-series constants

Used byTaylor expansion of Ramanujan's extension at the origin · Ramanujan's extension of the partial sums of a smooth function

DefinitionPartial sums of a real function over the positive integers#✓fully proved

For \(f : \mathbb{R} \to \mathbb{R}\) and a natural number \(n\), the partial sum is \(f(1) + f(2) + \cdots + f(n)\), which is \(0\) when \(n = 0\).

def chapter6PartialSum (f : ℝ → ℝ) (x : ℕ) : ℝ :=
  ∑ k ∈ Icc 1 x, f k

Used by 2

Used byRamanujan's extension agrees with the partial sums at natural numbers · Ramanujan's extension of the partial sums of a smooth function

TheoremThe derivative-series constant is the sum of its series#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(q\) be a natural number, and let \(f^{(q)}\) be the \(q\)-th iterated derivative of \(f\), where a derivative that does not exist is taken to be \(0\). If the family \(\bigl(f^{(q)}(k + 1)\bigr)_{k \in \mathbb{N}}\) is summable, then its sum is the constant \(c_q = \sum_{k \ge 1} f^{(q)}(k)\).

theorem hasSum_chapter6DerivedSeriesConstant (f : ℝ → ℝ) (q : ℕ)
    (h : Summable (chapter6ShiftedDerivedSeriesTerm f q 0)) :
    HasSum (chapter6ShiftedDerivedSeriesTerm f q 0) (chapter6DerivedSeriesConstant f q)

Uses 2 · Used by 1

Statement usesRamanujan's derivative-series constants · Terms of the shifted derivative series

Used byRamanujan's extension of the partial sums of a smooth function

TheoremDifference equation for Ramanujan's extension#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and let \(F(y) = \sum_{k \ge 1} f(k) - \sum_{k \ge 1} f(k + y)\), where a series that is not summable is given the value \(0\). If \(x \in \mathbb{R}\) and the series \(\sum_{k \ge 0} f(k + x)\) is summable, then \(F(x) - F(x - 1) = f(x)\).

theorem chapter6ConvergentSumExtension_sub_sub_one (f : ℝ → ℝ) (x : ℝ)
    (h : Summable (chapter6ShiftedDerivedSeriesTerm f 0 (x - 1))) :
    chapter6ConvergentSumExtension f x - chapter6ConvergentSumExtension f (x - 1) = f x

Uses 3 · Used by 2

Statement usesRamanujan's extension of partial sums · Terms of the shifted derivative series

Proof usesRamanujan's derivative-series constants

Used byRamanujan's extension agrees with the partial sums at natural numbers · Ramanujan's extension of the partial sums of a smooth function

TheoremTails of the shifted series of derivatives converge#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and \(q \in \mathbb{N}\), and write \(f^{(q)}\) for the \(q\)-th iterated derivative of \(f\), where a derivative that does not exist is taken to be \(0\). If the series \(\sum_{k \ge 0} f^{(q)}(k + 1)\) converges absolutely, then for every \(m \in \mathbb{N}\) the series \(\sum_{k \ge 0} f^{(q)}(k + 1 + m)\) converges absolutely.

The second series is the \(m\)-th tail of the first.

theorem summable_chapter6ShiftedDerivedSeriesTerm_natCast (f : ℝ → ℝ) (q : ℕ)
    (h : Summable (chapter6ShiftedDerivedSeriesTerm f q 0)) (m : ℕ) :
    Summable (chapter6ShiftedDerivedSeriesTerm f q m)

Uses 1 · Used by 1

Statement usesTerms of the shifted derivative series

Used byRamanujan's extension agrees with the partial sums at natural numbers

TheoremRamanujan's extension agrees with the partial sums at natural numbers#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and let \(F(x) = \sum_{k \ge 1} f(k) - \sum_{k \ge 1} f(k + x)\), where a series that is not summable is given the value \(0\). If the series \(\sum_{k \ge 1} f(k)\) is summable, then \(F(m) = f(1) + f(2) + \cdots + f(m)\) for every natural number \(m\) (for \(m = 0\) the right side is the empty sum \(0\)).

theorem chapter6ConvergentSumExtension_natCast (f : ℝ → ℝ)
    (h : Summable (chapter6ShiftedDerivedSeriesTerm f 0 0)) (m : ℕ) :
    chapter6ConvergentSumExtension f m = chapter6PartialSum f m

Uses 6 · Used by 1

Statement usesRamanujan's extension of partial sums · Partial sums of a real function over the positive integers · Terms of the shifted derivative series

Proof usesDifference equation for Ramanujan's extension · Ramanujan's derivative-series constants · Tails of the shifted series of derivatives converge

Used byRamanujan's extension of the partial sums of a smooth function

TheoremDerivatives of Ramanujan's extension at the origin#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be infinitely differentiable and let \(\rho > 0\). Write \(c_q = \sum_{k \ge 1} f^{(q)}(k)\) and \(F(x) = c_0 - \sum_{k \ge 1} f(k + x)\), where a series that is not summable is given the value \(0\). Suppose that the series \(\sum_{k \ge 1} f^{(q)}(k)\) is summable for every \(q \ge 0\), and that for every \(q \ge 1\) there is a summable sequence \((b_k)_{k \ge 0}\) with \(|f^{(q)}(k + 1 + x)| \le b_k\) for all \(x \in [-\rho, \rho]\) and all \(k \ge 0\). Then \(F^{(n)}(0) = -c_n\) for every natural number \(n \ge 1\).

theorem iteratedDeriv_chapter6ConvergentSumExtension_apply_zero (f : ℝ → ℝ) (rho : ℝ)
    (hrho : 0 < rho) (hsmooth : ContDiff ℝ ∞ f)
    (hsummable : ∀ q : ℕ, Summable (chapter6ShiftedDerivedSeriesTerm f q 0))
    (hdominated : ∀ q : ℕ, 0 < q → ∃ bound : ℕ → ℝ,
      Summable bound ∧
        ∀ x ∈ Set.Icc (-rho) rho, ∀ k : ℕ,
          |chapter6ShiftedDerivedSeriesTerm f q x k| ≤ bound k)
    (n : ℕ) (hn : 0 < n) :
    iteratedDeriv n (chapter6ConvergentSumExtension f) 0 =
      -chapter6DerivedSeriesConstant f n

Uses 3 · Used by 2

Statement usesRamanujan's extension of partial sums · Ramanujan's derivative-series constants · Terms of the shifted derivative series

Used byTaylor expansion of Ramanujan's extension at the origin · Ramanujan's extension of the partial sums of a smooth function

TheoremTaylor expansion of Ramanujan's extension at the origin#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be infinitely differentiable and let \(\rho > 0\). Write \(c_q = \sum_{k \ge 1} f^{(q)}(k)\) and \(F(x) = c_0 - \sum_{k \ge 1} f(k + x)\), where a series that is not summable is given the value \(0\). Suppose that the series \(\sum_{k \ge 1} f^{(q)}(k)\) is summable for every \(q \ge 0\), that for every \(q \ge 1\) there is a summable sequence \((b_k)_{k \ge 0}\) with \(|f^{(q)}(k + 1 + x)| \le b_k\) for all \(x \in [-\rho, \rho]\) and all \(k \ge 0\), and that \(F\) is analytic at \(0\). Then there is \(r\) with \(0 < r \le \rho\) such that for every real \(x\) with \(|x| < r\) the series \(\sum_{j \ge 0} -c_{j+1} x^{j+1} / (j+1)!\) is summable with sum \(F(x)\).

theorem exists_hasSum_chapter6Entry6Term (f : ℝ → ℝ) (rho : ℝ) (hrho : 0 < rho)
    (hsmooth : ContDiff ℝ ∞ f)
    (hsummable : ∀ q : ℕ, Summable (chapter6ShiftedDerivedSeriesTerm f q 0))
    (hdominated : ∀ q : ℕ, 0 < q → ∃ bound : ℕ → ℝ,
      Summable bound ∧
        ∀ x ∈ Set.Icc (-rho) rho, ∀ k : ℕ,
          |chapter6ShiftedDerivedSeriesTerm f q x k| ≤ bound k)
    (hanalytic : AnalyticAt ℝ (chapter6ConvergentSumExtension f) 0) :
    ∃ r : ℝ, 0 < r ∧ r ≤ rho ∧ ∀ x : ℝ, |x| < r →
      HasSum (chapter6Entry6Term f x) (chapter6ConvergentSumExtension f x)

Uses 5 · Used by 1

Statement usesRamanujan's extension of partial sums · Terms of the Taylor series in Entry 6 · Terms of the shifted derivative series

Proof usesRamanujan's derivative-series constants · Derivatives of Ramanujan's extension at the origin

Used byRamanujan's extension of the partial sums of a smooth function

TheoremRamanujan's extension of the partial sums of a smooth function#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be infinitely differentiable and let \(\rho > 0\). Suppose that for every \(q \in \mathbb{N}\) and every \(x \in \mathbb{R}\) the series \(\sum_{k \ge 0} f^{(q)}(k + 1 + x)\) converges absolutely, and that for every \(q \in \mathbb{N}\) there is a summable sequence \((b_k)_{k \ge 0}\) with \(|f^{(q)}(k + 1 + x)| \le b_k\) for all \(k \in \mathbb{N}\) and all \(x \in [-\rho, \rho]\). Put \(c_q = \sum_{k \ge 0} f^{(q)}(k + 1)\) and \(F(x) = c_0 - \sum_{k \ge 0} f(k + 1 + x)\), and suppose that \(F\) is analytic at \(0\). Then (i) for every \(n \in \mathbb{N}\) the series \(\sum_{k \ge 0} f^{(n)}(k + 1)\) converges absolutely with sum \(c_n\); (ii) \(F(0) = 0\); (iii) \(F(x) - F(x - 1) = f(x)\) for every \(x \in \mathbb{R}\); (iv) \(F(m) = f(1) + f(2) + \dots + f(m)\) for every \(m \in \mathbb{N}\), the empty sum being \(0\); (v) \(F^{(n)}(0) = -c_n\) for every integer \(n \ge 1\); and (vi) there is \(r\) with \(0 < r \le \rho\) such that for every real \(x\) with \(|x| < r\) the series \(\sum_{j \ge 0} -c_{j+1} x^{j+1} / (j + 1)!\) converges absolutely with sum \(F(x)\).

MathlibExt.Analysis.Ramanujan.Part1Ch6.Entry6Harmonic.ramanujan_part1_ch6_entry6_harmonic · 23 lines

theorem ramanujan_part1_ch6_entry6_harmonic
    (f : ℝ → ℝ) (rho : ℝ) (hrho : 0 < rho)
    (hsmooth : ContDiff ℝ ∞ f)
    (hsummable : ∀ q : ℕ, ∀ x : ℝ,
      Summable (chapter6ShiftedDerivedSeriesTerm f q x))
    (hdominated : ∀ q : ℕ, ∃ bound : ℕ → ℝ,
      Summable bound ∧
        ∀ x ∈ Set.Icc (-rho) rho, ∀ k : ℕ,
          |chapter6ShiftedDerivedSeriesTerm f q x k| ≤ bound k)
    (hanalytic : AnalyticAt ℝ (chapter6ConvergentSumExtension f) 0) :
    (∀ n : ℕ, HasSum (chapter6ShiftedDerivedSeriesTerm f n 0)
      (chapter6DerivedSeriesConstant f n)) ∧
      chapter6ConvergentSumExtension f 0 = 0 ∧
      (∀ x : ℝ, chapter6ConvergentSumExtension f x -
        chapter6ConvergentSumExtension f (x - 1) = f x) ∧
      (∀ m : ℕ, chapter6ConvergentSumExtension f m = chapter6PartialSum f m) ∧
      (∀ n : ℕ, 0 < n →
        iteratedDeriv n (chapter6ConvergentSumExtension f) 0 =
          -chapter6DerivedSeriesConstant f n) ∧
      ∃ r : ℝ, 0 < r ∧ r ≤ rho ∧
        ∀ x : ℝ, |x| < r →
          HasSum (chapter6Entry6Term f x)
            (chapter6ConvergentSumExtension f x)

Sources

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

Uses 10

Statement usesRamanujan's extension of partial sums · Ramanujan's derivative-series constants · Terms of the Taylor series in Entry 6 · Partial sums of a real function over the positive integers · Terms of the shifted derivative series

Proof usesRamanujan's extension agrees with the partial sums at natural numbers · Difference equation for Ramanujan's extension · Taylor expansion of Ramanujan's extension at the origin · The derivative-series constant is the sum of its series · Derivatives of Ramanujan's extension at the origin

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.