Berndt's power-difference function φᵣ

TheoremThe Entry 10 zeta factor in Bernoulli form#✓fully proved

Let \(n\) be a positive integer, and for \(z \in \mathbb{C}\) put \(B^*(z) = 2\,\Gamma(z + 1)\,\zeta(z) / (2\pi)^z\). Then the functions \(Z(r) = (1 - n^{r+1})\,\zeta(-r)\) and \(B(r) = (n^{r+1} - 1) \sin(\pi r / 2)\, B^*(r + 1) / (r + 1)\) are meromorphic on \(\mathbb{C}\), and \(Z(r) = B(r)\) for all \(r \in \mathbb{C}\) outside a closed discrete subset of \(\mathbb{C}\).

theorem ramanujan_part1_ch7_entry10_zeta4 (n : ℕ) (hn : 0 < n) :
    MeromorphicOn (chapter7Entry10ZetaSide n) Set.univ ∧
      MeromorphicOn (chapter7Entry10BernoulliSide n) Set.univ ∧
      chapter7Entry10ZetaSide n =ᶠ[codiscrete ℂ]
        chapter7Entry10BernoulliSide n

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 10.

Uses 1

Proof usesMeromorphy of the Riemann zeta function

TheoremBernoulli-number expansion of a Bernoulli-polynomial difference#✓fully proved

For every positive integer \(r\) and every \(x \in \mathbb{C}\), \(\frac{B_{r+1}(x + 1) - B_{r+1}(1)}{r + 1}\) equals \(\frac{1}{r + 1} \sum_{k=0}^{r} \binom{r+1}{k} B_k\, x^{r+1-k} + x^r\), where \(B_{r+1}(x)\) is the Bernoulli polynomial and \(B_k\) are the Bernoulli numbers with \(B_1 = -\tfrac12\).

theorem ramanujan_part1_ch7_entry8 (r : ℕ) (hr : 0 < r) (x : ℂ) :
    ((Polynomial.bernoulli (r + 1)).eval₂ (algebraMap ℚ ℂ) (x + 1) -
      (Polynomial.bernoulli (r + 1)).eval₂ (algebraMap ℚ ℂ) 1) / (r + 1 : ℂ) =
    (∑ k ∈ range (r + 1),
        ((r + 1).choose k : ℂ) * (bernoulli k : ℂ) * x ^ (r + 1 - k)) /
        (r + 1 : ℂ) + x ^ r

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 8.

Used by 1

Used byBernoulli and zeta expansions of \(P_r\), and sums of powers

DefinitionArguments of Berndt's \(\varphi_r(x)\)#✓fully proved

The open interval \((-1, 0)\) of real numbers, that is, the set of real \(x\) with \(-1 < x < 0\).

On this interval \(x + 1\) lies in \((0, 1)\), so the Hurwitz zeta function at parameter \(x + 1\) is not affected by reduction modulo \(1\).

def Chapter7PhiArgument := Set.Ioo (-1 : ℝ) 0

Used by 8

Used byBerndt's function \(\varphi_r(x)\) on \((-1, 0)\) · Berndt's \(\varphi_r\) as a Bernoulli-polynomial difference for positive integer \(r\) · A sine series for \(\varphi_r(x-1) - \varphi_r(-x)\) · A cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\) · \(\varphi_r(-1/4) - \varphi_r(-3/4)\) through the Dirichlet beta function · Ramanujan's functional equation for \(\varphi\) at rationals with odd denominator · Ramanujan's functional equation for \(\varphi\) at \(-1/3\) and \(-2/3\) · Bernoulli and zeta expansions of Berndt's \(\varphi_r\) on \((-1, 0)\)

DefinitionBerndt's function \(\varphi_r(x)\) on \((-1, 0)\)#✓fully proved

For a complex number \(r\) and a real number \(x\) with \(-1 < x < 0\), \(\varphi_r(x) = \zeta(-r) - \zeta(-r, x + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) is the Hurwitz zeta function, both analytically continued in \(s\). At \(r = -1\), where both have a pole, \(\zeta(1)\) and \(\zeta(1, x + 1)\) denote the finite values that the formal definitions assign at the pole.

On this interval \(x + 1\) lies in \((0, 1)\), so the Hurwitz zeta function at parameter \(x + 1\) is not affected by reduction modulo \(1\).

noncomputable def chapter7Phi (r : ℂ) (x : Chapter7PhiArgument) : ℂ :=
  riemannZeta (-r) -
    HurwitzZeta.hurwitzZeta (((x : ℝ) + 1 : ℝ) : UnitAddCircle) (-r)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, equation (2.4), p. 152.

Uses 1 · Used by 7

Statement usesArguments of Berndt's \(\varphi_r(x)\)

Used byBerndt's \(\varphi_r\) as a Bernoulli-polynomial difference for positive integer \(r\) · A sine series for \(\varphi_r(x-1) - \varphi_r(-x)\) · A cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\) · \(\varphi_r(-1/4) - \varphi_r(-3/4)\) through the Dirichlet beta function · Ramanujan's functional equation for \(\varphi\) at rationals with odd denominator · Ramanujan's functional equation for \(\varphi\) at \(-1/3\) and \(-2/3\) · Bernoulli and zeta expansions of Berndt's \(\varphi_r\) on \((-1, 0)\)

TheoremA sine series for \(\varphi_r(x-1) - \varphi_r(-x)\)#✓fully proved

For complex \(r\) and real \(-1 < y < 0\) let \(\varphi_r(y) = \zeta(-r) - \zeta(-r, y + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) is the Hurwitz zeta function. Let \(r\) be a complex number with \(\operatorname{Re} r > -1\) and let \(0 < x < 1\). Then the partial sums of \(\sum_{k \ge 1} \sin(2\pi k x) / (2\pi k)^{r+1}\) converge to a limit \(L\), and

\[\frac{\varphi_r(x-1) - \varphi_r(-x)}{4\,\Gamma(r+1)} = -\cos\left(\frac{\pi r}{2}\right) L.\]

theorem ramanujan_part1_ch7_entry15_vonstaudtclausen
    (r : ℂ) (x : ℝ) (hr : -1 < r.re) (hx0 : 0 < x) (hx1 : x < 1) :
    ∃! L : ℂ,
      Tendsto (chapter7Entry15PartialSum r x) atTop (𝓝 L) ∧
        chapter7Entry15Left r x hx0 hx1 =
          -Complex.cos ((Real.pi : ℂ) * r / 2) * L

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 15.

Uses 2

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

TheoremA cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\)#✓fully proved

For complex \(r\) and real \(-1 < y < 0\) let \(\varphi_r(y) = \zeta(-r) - \zeta(-r, y + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) is the Hurwitz zeta function. Let \(r\) be a complex number with \(\operatorname{Re} r > -1\) and let \(0 < x < 1\). Then the partial sums of \(\sum_{k \ge 1} \cos(2\pi k x) / (2\pi k)^{r+1}\) converge to a limit \(L\), and

\[\frac{\varphi_r(x-1) + \varphi_r(-x) - 2\zeta(-r)}{4\,\Gamma(r+1)} = \sin\left(\frac{\pi r}{2}\right) L.\]

theorem ramanujan_part1_ch7_entry16_kummercongruence
    (r : ℂ) (x : ℝ) (hr : -1 < r.re) (hx0 : 0 < x) (hx1 : x < 1) :
    ∃! L : ℂ,
      Tendsto (chapter7Entry16PartialSum r x) atTop (𝓝 L) ∧
        chapter7Entry16Left r x hx0 hx1 =
          Complex.sin ((Real.pi : ℂ) * r / 2) * L

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 16.

Uses 7

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

Proof usesAbel continuation of a Dirichlet series · Abel continuation agrees with the Dirichlet series · Partial sums of a coefficient sequence · Analyticity of the Abel continuation · Abel continuation as the limit of Dirichlet partial sums

Theorem\(\varphi_r(-1/4) - \varphi_r(-3/4)\) through the Dirichlet beta function#✓fully proved

Let \(\chi\) be the function on \(\mathbb{Z}/4\mathbb{Z}\) with \(\chi(1) = 1\), \(\chi(3) = -1\) and \(\chi(0) = \chi(2) = 0\), let \(\beta\) be its Dirichlet \(L\)-function (analytically continued to \(\mathbb{C}\)), and let \(E^*(s) = 2\,\Gamma(s)\,\beta(s) / (\pi/2)^s\). For complex \(r\) and real \(-1 < y < 0\) let \(\varphi_r(y) = \zeta(-r) - \zeta(-r, y + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) is the Hurwitz zeta function, and put

\[\ell(r) = \varphi_r(-1/4) - \varphi_r(-3/4), \qquad \rho(r) = \frac{2 \cos(\pi r / 2)\, E^*(r+1)}{4^{r+1}}.\]

Then \(\beta\) is entire; for every complex \(s\) with \(\operatorname{Re} s > 0\) the partial sums \(\sum_{k=0}^{N-1} (-1)^k / (2k+1)^s\) tend to \(\beta(s)\) as \(N \to \infty\); \(E^*\), \(\ell\) and \(\rho\) are meromorphic on \(\mathbb{C}\); and \(\ell(r) = \rho(r)\) for all \(r\) outside a closed discrete subset of \(\mathbb{C}\).

theorem ramanujan_part1_ch7_entry17_bernoullipolysymmetry :
    Differentiable ℂ chapter7DirichletBeta ∧
      (∀ s : ℂ, 0 < s.re →
        Tendsto (chapter7DirichletBetaPartialSum s) atTop
          (𝓝 (chapter7DirichletBeta s))) ∧
      MeromorphicOn chapter7EulerStar Set.univ ∧
      MeromorphicOn chapter7Entry17Left Set.univ ∧
      MeromorphicOn chapter7Entry17Right Set.univ ∧
      chapter7Entry17Left =ᶠ[codiscrete ℂ] chapter7Entry17Right

Sources

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

Uses 2

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

TheoremRamanujan's functional equation for \(\varphi\) at rationals with odd denominator#✓fully proved

For \(-1 < x < 0\) and \(r \in \mathbb{C}\) let \(\varphi_r(x) = \zeta(-r) - \zeta(-r, x + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) the Hurwitz zeta function. Let \(p\) and \(q\) be natural numbers with \(0 < p < q\) and \(q\) odd, and for \(r \in \mathbb{C}\) put \(L(r) = \frac{(2\pi q)^r}{4\,\Gamma(r)} \bigl(\varphi_{r-1}(p/q - 1) - \varphi_{r-1}(-p/q)\bigr)\) and \(R(r) = \sin(\pi r/2) \sum_{j=1}^{(q-1)/2} \sin(2\pi j p/q)\, D_j(r)\), where \(D_j(r) = \varphi_{-r}(j/q - 1) - \varphi_{-r}(-j/q)\). Then \(L\) and \(R\) are meromorphic on \(\mathbb{C}\) and agree outside a closed discrete subset of \(\mathbb{C}\).

theorem ramanujan_part1_ch7_entry19_zetanegint
    (p q : ℕ) (hp : 0 < p) (hpq : p < q) (hq : Odd q) :
    MeromorphicOn (chapter7Entry19Left p q hp hpq) Set.univ ∧
      MeromorphicOn (chapter7Entry19Right p q) Set.univ ∧
      (chapter7Entry19Left p q hp hpq) =ᶠ[codiscrete ℂ]
        (chapter7Entry19Right p q)

Sources

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

Uses 2

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

TheoremRamanujan's functional equation for \(\varphi\) at \(-1/3\) and \(-2/3\)#✓fully proved

For \(-1 < x < 0\) and \(r \in \mathbb{C}\) let \(\varphi_r(x) = \zeta(-r) - \zeta(-r, x + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) the Hurwitz zeta function. Then the functions \(L(r) = \frac{(6\pi)^r}{2\sqrt{3}\,\Gamma(r)} \bigl(\varphi_{r-1}(-1/3) - \varphi_{r-1}(-2/3)\bigr)\) and \(R(r) = \sin(\pi r/2) \bigl(\varphi_{-r}(-1/3) - \varphi_{-r}(-2/3)\bigr)\) of \(r \in \mathbb{C}\) are meromorphic on \(\mathbb{C}\) and agree outside a closed discrete subset of \(\mathbb{C}\).

theorem ramanujan_part1_ch7_entry20_generalizedbernoullisum :
    MeromorphicOn chapter7Entry20Left Set.univ ∧
      MeromorphicOn chapter7Entry20Right Set.univ ∧
      chapter7Entry20Left =ᶠ[codiscrete ℂ] chapter7Entry20Right

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 20.

Uses 2

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

DefinitionBernoulli-polynomial form of Berndt's \(\varphi_r\)#✓fully proved

For a natural number \(r\) and \(x \in \mathbb{C}\), \(P_r(x) = \frac{B_{r+1}(x + 1) - B_{r+1}(1)}{r + 1}\), where \(B_{r+1}\) is the Bernoulli polynomial of degree \(r + 1\).

For positive \(r\) this polynomial agrees on \(-1 < x < 0\) with Berndt's \(\varphi_r(x) = \zeta(-r) - \zeta(-r, x + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) the Hurwitz zeta function, and so extends it to all of \(\mathbb{C}\).

def chapter7IntegerPhi (r : ℕ) (x : ℂ) : ℂ :=
  (chapter7BernoulliPolynomial (r + 1) (x + 1) -
      chapter7BernoulliPolynomial (r + 1) 1) /
    (r + 1 : ℂ)

Used by 4

Used byBerndt's \(\varphi_r\) as a Bernoulli-polynomial difference for positive integer \(r\) · Bernoulli and zeta expansions of \(P_r\), and sums of powers · Bernoulli and zeta expansions of Berndt's \(\varphi_r\) on \((-1, 0)\) · Entire continuations of the power-difference series agree and take Bernoulli values

TheoremBernoulli and zeta expansions of \(P_r\), and sums of powers#✓fully proved

Let \(r\) be a positive integer and \(P_r(x) = \frac{B_{r+1}(x + 1) - B_{r+1}(1)}{r + 1}\), where \(B_{r+1}\) is the Bernoulli polynomial of degree \(r + 1\). Then for every \(x \in \mathbb{C}\), \(P_r(x) = \frac{1}{r + 1} \sum_{k=0}^{r} \binom{r+1}{k} B_k\, x^{r+1-k} + x^r\), where \(B_k\) are the Bernoulli numbers with \(B_1 = -\tfrac12\), and \(P_r(x) = \frac{x^{r+1}}{r + 1} + \frac{x^r}{2} - \frac{2}{r + 1} Z_r(x)\), where \(Z_r(x) = \sum_{k=1}^{\lfloor r/2 \rfloor} \binom{r+1}{2k}\, k\, \zeta(1 - 2k)\, x^{r+1-2k}\) and \(\zeta\) is the Riemann zeta function. Moreover \(P_r(n) = \sum_{k=1}^{n} k^r\) for every natural number \(n\).

theorem ramanujan_part1_ch7_entry8_bernoullibound
    (r : ℕ) (hr : 0 < r) (x : ℂ) :
    chapter7IntegerPhi r x = chapter7Entry8BernoulliForm r x ∧
      chapter7IntegerPhi r x = chapter7Entry8ZetaForm r x ∧
      ∀ n : ℕ,
        chapter7IntegerPhi r n = ∑ k ∈ Icc 1 n, (k : ℂ) ^ r

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 8.

Uses 2 · Used by 1

Statement usesBernoulli-polynomial form of Berndt's \(\varphi_r\)

Proof usesBernoulli-number expansion of a Bernoulli-polynomial difference

Used byBernoulli and zeta expansions of Berndt's \(\varphi_r\) on \((-1, 0)\)

TheoremBerndt's \(\varphi_r\) as a Bernoulli-polynomial difference for positive integer \(r\)#✓fully proved

Let \(r\) be a positive integer and \(-1 < x < 0\). Then \(\varphi_r(x) = \zeta(-r) - \zeta(-r, x + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) the Hurwitz zeta function, equals \(P_r(x) = \frac{B_{r+1}(x + 1) - B_{r+1}(1)}{r + 1}\), where \(B_{r+1}\) is the Bernoulli polynomial of degree \(r + 1\).

theorem chapter7Phi_eq_chapter7IntegerPhi (r : ℕ) (hr : r ≠ 0) (x : Chapter7PhiArgument) :
    chapter7Phi r x = chapter7IntegerPhi r (x : ℝ)

Uses 3 · Used by 1

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Bernoulli-polynomial form of Berndt's \(\varphi_r\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

Used byBernoulli and zeta expansions of Berndt's \(\varphi_r\) on \((-1, 0)\)

TheoremBernoulli and zeta expansions of Berndt's \(\varphi_r\) on \((-1, 0)\)#✓fully proved

Let \(r\) be a positive integer and, for \(-1 < x < 0\), let \(\varphi_r(x) = \zeta(-r) - \zeta(-r, x + 1)\), where \(\zeta\) is the Riemann zeta function and \(\zeta(s, a)\) the Hurwitz zeta function. Then for every \(-1 < x < 0\), \(\varphi_r(x) = \frac{1}{r + 1} \sum_{k=0}^{r} \binom{r+1}{k} B_k\, x^{r+1-k} + x^r\), where \(B_k\) are the Bernoulli numbers with \(B_1 = -\tfrac12\), and \(\varphi_r(x) = \frac{x^{r+1}}{r + 1} + \frac{x^r}{2} - \frac{2}{r + 1} Z_r(x)\), where \(Z_r(x) = \sum_{k=1}^{\lfloor r/2 \rfloor} \binom{r+1}{2k}\, k\, \zeta(1 - 2k)\, x^{r+1-2k}\).

theorem ramanujan_part1_ch7_entry8_phi (r : ℕ) (hr : 0 < r) (x : Chapter7PhiArgument) :
    chapter7Phi r x = chapter7Entry8BernoulliForm r (x : ℝ) ∧
      chapter7Phi r x = chapter7Entry8ZetaForm r (x : ℝ)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 8, for Berndt's φ_r (chapter7Phi) on its domain -1 < x < 0.

Uses 5

Statement usesArguments of Berndt's \(\varphi_r(x)\) · Berndt's function \(\varphi_r(x)\) on \((-1, 0)\)

Proof usesBernoulli-polynomial form of Berndt's \(\varphi_r\) · Berndt's \(\varphi_r\) as a Bernoulli-polynomial difference for positive integer \(r\) · Bernoulli and zeta expansions of \(P_r\), and sums of powers

DefinitionAdmissible parameters for the power-difference series#✓fully proved

A complex number \(x\) is admissible when \(j + 1 + x \ne 0\) for every natural number \(j\), that is, when \(x\) is not one of \(-1, -2, -3, \dots\).

def chapter7Admissible (x : ℂ) : Prop :=
  ∀ j : ℕ, (j + 1 : ℂ) + x ≠ 0

Used by 8

Used byAdmissibility in the corollary of Ramanujan's Entry 10 · Admissibility in Ramanujan's Entry 9 · The points \(-k/n\) are admissible · Zero is admissible · The corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\) · Ramanujan's corollary to Entry 10 of Chapter 7 · Convergence and holomorphy of the power-difference series · Entire continuations of the power-difference series agree and take Bernoulli values

DefinitionTerms of the power-difference series#✓fully proved

For complex numbers \(r\) and \(x\) and a natural number \(j\), the \(j\)-th term is \((j + 1)^r - (j + 1 + x)^r\), where \(w^r = e^{r \log w}\) is the principal power for \(w \ne 0\), while \(0^r = 0\) for \(r \ne 0\) and \(0^0 = 1\).

def chapter7PowerDifferenceTerm (r x : ℂ) (j : ℕ) : ℂ :=
  Complex.cpow (j + 1 : ℂ) r - Complex.cpow ((j + 1 : ℂ) + x) r

Used by 11

Used byThe corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\) · The power-difference series · Power difference term in Ramanujan's Entry 10 · Power difference term in the corollary of Entry 10 · Power difference term in Ramanujan's Entry 9 · Power-difference terms vanish at exponent zero · Power-difference terms vanish at \(x = 0\) · Ramanujan's distribution relation for the power-difference function · Ramanujan's corollary to Entry 10 of Chapter 7 · Convergence and holomorphy of the power-difference series · Entire continuations of the power-difference series agree and take Bernoulli values

DefinitionThe power-difference series#✓fully proved

For complex numbers \(r\) and \(x\), \(\varphi_r(x) = \sum_{j \ge 0} \bigl((j + 1)^r - (j + 1 + x)^r\bigr)\) (principal powers), where the sum is taken to be \(0\) when the series is not summable.

def chapter7PowerDifferenceSum (r x : ℂ) : ℂ :=
  ∑' j : ℕ, chapter7PowerDifferenceTerm r x j

Uses 1 · Used by 2

Statement usesTerms of the power-difference series

Used byPower difference sum in Ramanujan's Entry 9 · Convergence and holomorphy of the power-difference series

TheoremRamanujan's distribution relation for the power-difference function#✓fully proved

Let \(\varphi : \mathbb{C} \times \mathbb{C} \to \mathbb{C}\), written \((r, x) \mapsto \varphi_r(x)\), be such that for every \(x \in \mathbb{C}\) the function \(r \mapsto \varphi_r(x)\) is meromorphic on \(\mathbb{C}\), and such that for all \(r, x \in \mathbb{C}\) with \(\operatorname{Re} r < 0\) the series \(\sum_{j \ge 0} \bigl((j + 1)^r - (j + 1 + x)^r\bigr)\) converges absolutely with sum \(\varphi_r(x)\). Let \(n\) be a positive integer and \(x \in \mathbb{C}\). Then the functions \(L(r) = \varphi_r(x) - n^r \sum_{k=0}^{n-1} \varphi_r\bigl((x - k)/n\bigr)\) and \(Z(r) = (1 - n^{r+1})\,\zeta(-r)\) are meromorphic on \(\mathbb{C}\), and \(L(r) = Z(r)\) for all \(r \in \mathbb{C}\) outside a closed discrete subset of \(\mathbb{C}\).

Complex powers are principal-branch powers: \(w^r = \exp(r \log w)\) for \(w \ne 0\), and \(0^r = 0\) for \(r \ne 0\).

theorem ramanujan_part1_ch7_entry10_zeta2
    (phi : ℂ → ℂ → ℂ)
    (hphi_meromorphic : ∀ x, MeromorphicOn (fun r : ℂ => phi r x) Set.univ)
    (hphi_series : ∀ r x, r.re < 0 → HasSum (chapter7PowerDifferenceTerm r x) (phi r x))
    (n : ℕ) (hn : 0 < n) (x : ℂ) :
    MeromorphicOn (chapter7Entry10DistributionLeft phi n x) Set.univ ∧
      MeromorphicOn (chapter7Entry10ZetaSide n) Set.univ ∧
      chapter7Entry10DistributionLeft phi n x =ᶠ[codiscrete ℂ]
        chapter7Entry10ZetaSide n

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 10.

Uses 2

Statement usesTerms of the power-difference series

Proof usesMeromorphy of the Riemann zeta function

AbbreviationPower difference term in Ramanujan's Entry 10#✓fully proved

The power-difference term of Ramanujan's Entry 10 is the \(j\)-th term of the power-difference series, \((j + 1)^r - (j + 1 + x)^r\).

noncomputable abbrev chapter7PowerDifferenceTerm (r x : ℂ) (j : ℕ) : ℂ :=
  MathlibExt.Analysis.Ramanujan.Part1Ch7.chapter7PowerDifferenceTerm r x j

Uses 1

Statement usesTerms of the power-difference series

DefinitionLeft side of the corollary to Entry 10#✓fully proved

For a function \(\varphi : \mathbb{C} \to \mathbb{C} \to \mathbb{C}\), a natural number \(n\) and \(r \in \mathbb{C}\), the left side of the corollary to Entry 10 is \(\sum_{k=1}^{n-1} \varphi(r, -k/n)\), the empty sum \(0\) when \(n \le 1\). In Berndt's notation, \(\varphi(r, x)\) is written \(\varphi_r(x)\).

def chapter7Entry10CorollaryLeft
    (phi : ℂ → ℂ → ℂ) (n : ℕ) (r : ℂ) : ℂ :=
  ∑ k ∈ Icc 1 (n - 1), phi r (-((k : ℂ) / n))

Used by 2

Used byThe corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\) · Ramanujan's corollary to Entry 10 of Chapter 7

DefinitionRight side of the corollary to Entry 10#✓fully proved

For a natural number \(n\) and \(r \in \mathbb{C}\), the right side of the corollary to Entry 10 is \((n - n^{-r})\,\zeta(-r)\), where \(n^{-r}\) is the principal complex power and \(\zeta\) is the Riemann zeta function.

def chapter7Entry10CorollaryRight (n : ℕ) (r : ℂ) : ℂ :=
  ((n : ℂ) - Complex.cpow (n : ℂ) (-r)) * riemannZeta (-r)

Used by 2

Used byThe corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\) · Ramanujan's corollary to Entry 10 of Chapter 7

TheoremThe points \(-k/n\) are admissible#✓fully proved

For natural numbers \(n\) and \(k\) with \(1 \le k \le n - 1\), the point \(x = -k/n\) is admissible, that is, \(j + 1 + x \neq 0\) for every natural number \(j\).

These are the points at which the left side of the corollary to Entry 10 evaluates \(\varphi\).

theorem chapter7Admissible_neg_div {n k : ℕ} (hk : k ∈ Finset.Icc 1 (n - 1)) :
    chapter7Admissible (-((k : ℂ) / (n : ℂ)))

Uses 1 · Used by 2

Statement usesAdmissible parameters for the power-difference series

Used byThe corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\) · Ramanujan's corollary to Entry 10 of Chapter 7

TheoremThe corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\)#✓fully proved

Call \(x \in \mathbb{C}\) admissible if \(j + 1 + x \neq 0\) for every natural number \(j\). Let \(\varphi : \mathbb{C} \to \mathbb{C} \to \mathbb{C}\) be such that, for every \(r \in \mathbb{C}\) with \(\operatorname{Re} r < 0\) and every admissible \(x\), the series \(\sum_{j \ge 0} \bigl((j + 1)^r - (j + 1 + x)^r\bigr)\) of principal complex powers is unconditionally summable with sum \(\varphi(r, x)\). Then for every natural number \(n\) and every \(r \in \mathbb{C}\) with \(\operatorname{Re} r < -1\), \(\sum_{k=1}^{n-1} \varphi(r, -k/n) = (n - n^{-r})\,\zeta(-r)\), where \(\zeta\) is the Riemann zeta function.

theorem chapter7Entry10CorollaryLeft_eq_right (phi : ℂ → ℂ → ℂ)
    (hphi_series : ∀ r x, r.re < 0 → chapter7Admissible x →
      HasSum (chapter7PowerDifferenceTerm r x) (phi r x))
    (n : ℕ) (r : ℂ) (hr : r.re < -1) :
    chapter7Entry10CorollaryLeft phi n r
      = chapter7Entry10CorollaryRight n r

Uses 5 · Used by 1

Statement usesLeft side of the corollary to Entry 10 · Right side of the corollary to Entry 10 · Admissible parameters for the power-difference series · Terms of the power-difference series

Proof usesThe points \(-k/n\) are admissible

Used byRamanujan's corollary to Entry 10 of Chapter 7

TheoremRamanujan's corollary to Entry 10 of Chapter 7#✓fully proved

Call \(x \in \mathbb{C}\) admissible if \(j + 1 + x \neq 0\) for every natural number \(j\). Let \(\varphi : \mathbb{C} \to \mathbb{C} \to \mathbb{C}\) be such that, for every admissible \(x\), the function \(r \mapsto \varphi(r, x)\) is entire, and, for every \(r \in \mathbb{C}\) with \(\operatorname{Re} r < 0\) and every admissible \(x\), the series \(\sum_{j \ge 0} \bigl((j + 1)^r - (j + 1 + x)^r\bigr)\) of principal complex powers is unconditionally summable with sum \(\varphi(r, x)\). Then for every positive integer \(n\) the functions \(L(r) = \sum_{k=1}^{n-1} \varphi(r, -k/n)\) and \(R(r) = (n - n^{-r})\,\zeta(-r)\), where \(\zeta\) is the Riemann zeta function, are meromorphic on \(\mathbb{C}\), and the set of \(r \in \mathbb{C}\) with \(L(r) \neq R(r)\) has no accumulation point in \(\mathbb{C}\).

theorem ramanujan_part1_ch7_entry10_zetaviabernoulli
    (phi : ℂ → ℂ → ℂ)
    (hphi_entire : ∀ x, chapter7Admissible x →
      Differentiable ℂ (fun r : ℂ => phi r x))
    (hphi_series : ∀ r x, r.re < 0 → chapter7Admissible x →
      HasSum (chapter7PowerDifferenceTerm r x) (phi r x))
    (n : ℕ) (hn : 0 < n) :
    MeromorphicOn (chapter7Entry10CorollaryLeft phi n) Set.univ ∧
      MeromorphicOn (chapter7Entry10CorollaryRight n) Set.univ ∧
      chapter7Entry10CorollaryLeft phi n =ᶠ[codiscrete ℂ]
        chapter7Entry10CorollaryRight n

Sources

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

Uses 7

Statement usesLeft side of the corollary to Entry 10 · Right side of the corollary to Entry 10 · Admissible parameters for the power-difference series · Terms of the power-difference series

Proof usesThe points \(-k/n\) are admissible · The corollary to Entry 10 in the half-plane \(\operatorname{Re} r < -1\) · Meromorphy of the Riemann zeta function

AbbreviationAdmissibility in the corollary of Ramanujan's Entry 10#✓fully proved

Admissibility in the corollary of Ramanujan's Entry 10 is admissibility for the power-difference series: \(x\) is not one of \(-1, -2, -3, \dots\).

abbrev chapter7Admissible (x : ℂ) : Prop :=
  MathlibExt.Analysis.Ramanujan.Part1Ch7.chapter7Admissible x

Uses 1 · Used by 1

Statement usesAdmissible parameters for the power-difference series

Used byZero is admissible

AbbreviationPower difference term in the corollary of Entry 10#✓fully proved

The power-difference term of the corollary of Ramanujan's Entry 10 is the \(j\)-th term of the power-difference series, \((j + 1)^r - (j + 1 + x)^r\).

noncomputable abbrev chapter7PowerDifferenceTerm (r x : ℂ) (j : ℕ) : ℂ :=
  MathlibExt.Analysis.Ramanujan.Part1Ch7.chapter7PowerDifferenceTerm r x j

Uses 1 · Used by 2

Statement usesTerms of the power-difference series

Used byPower-difference terms vanish at exponent zero · Power-difference terms vanish at \(x = 0\)

TheoremZero is admissible#✓fully proved

The point \(x = 0\) is admissible: \(j + 1 + x \neq 0\) for every natural number \(j\).

@[simp]
theorem chapter7Admissible_zero : chapter7Admissible 0

Uses 2

Statement usesAdmissibility in the corollary of Ramanujan's Entry 10

Proof usesAdmissible parameters for the power-difference series

TheoremPower-difference terms vanish at exponent zero#✓fully proved

For every \(x \in \mathbb{C}\) and every natural number \(j\), the power-difference term \((j + 1)^r - (j + 1 + x)^r\) vanishes at \(r = 0\).

@[simp]
theorem chapter7PowerDifferenceTerm_zero_left (x : ℂ) (j : ℕ) :
    chapter7PowerDifferenceTerm 0 x j = 0

Uses 2

Statement usesPower difference term in the corollary of Entry 10

Proof usesTerms of the power-difference series

TheoremPower-difference terms vanish at \(x = 0\)#✓fully proved

For every \(r \in \mathbb{C}\) and every natural number \(j\), the power-difference term \((j + 1)^r - (j + 1 + x)^r\) vanishes at \(x = 0\).

@[simp]
theorem chapter7PowerDifferenceTerm_zero_right (r : ℂ) (j : ℕ) :
    chapter7PowerDifferenceTerm r 0 j = 0

Uses 2

Statement usesPower difference term in the corollary of Entry 10

Proof usesTerms of the power-difference series

TheoremConvergence and holomorphy of the power-difference series#✓fully proved

Let \(x\) be an admissible complex number. For every complex \(r\) with \(\operatorname{Re} r < 0\) the series \(\sum_{j \ge 0} \bigl((j + 1)^r - (j + 1 + x)^r\bigr)\) (principal powers) is summable, and its sum \(\varphi_r(x)\) is a holomorphic function of \(r\) on the half-plane \(\operatorname{Re} r < 0\).

theorem ramanujan_part1_ch7_entry9_bernoulligrowth
    (x : ℂ) (hx : chapter7Admissible x) :
    (∀ r : ℂ, r.re < 0 → Summable (chapter7PowerDifferenceTerm r x)) ∧
      DifferentiableOn ℂ (fun r : ℂ => chapter7PowerDifferenceSum r x)
        {r : ℂ | r.re < 0}

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 9.

Uses 3

Statement usesAdmissible parameters for the power-difference series · The power-difference series · Terms of the power-difference series

AbbreviationAdmissibility in Ramanujan's Entry 9#✓fully proved

Admissibility in Ramanujan's Entry 9 is admissibility for the power-difference series: \(x\) is not one of \(-1, -2, -3, \dots\).

abbrev chapter7Admissible (x : ℂ) : Prop :=
  MathlibExt.Analysis.Ramanujan.Part1Ch7.chapter7Admissible x

Uses 1

Statement usesAdmissible parameters for the power-difference series

AbbreviationPower difference term in Ramanujan's Entry 9#✓fully proved

The power-difference term of Ramanujan's Entry 9 is the \(j\)-th term of the power-difference series, \((j + 1)^r - (j + 1 + x)^r\).

noncomputable abbrev chapter7PowerDifferenceTerm (r x : ℂ) (j : ℕ) : ℂ :=
  MathlibExt.Analysis.Ramanujan.Part1Ch7.chapter7PowerDifferenceTerm r x j

Uses 1

Statement usesTerms of the power-difference series

AbbreviationPower difference sum in Ramanujan's Entry 9#✓fully proved

The power-difference sum of Ramanujan's Entry 9 is the power-difference series \(\varphi_r(x)\).

noncomputable abbrev chapter7PowerDifferenceSum (r x : ℂ) : ℂ :=
  MathlibExt.Analysis.Ramanujan.Part1Ch7.chapter7PowerDifferenceSum r x

Uses 1

Statement usesThe power-difference series

TheoremEntire continuations of the power-difference series agree and take Bernoulli values#✓fully proved

Let \(f\) and \(g\) be complex-valued functions of two complex variables \((r, x)\) such that, for every admissible \(x\), both \(r \mapsto f(r, x)\) and \(r \mapsto g(r, x)\) are entire, and for every admissible \(x\) and every complex \(r\) with \(\operatorname{Re} r < 0\) the series \(\sum_{j \ge 0} \bigl((j + 1)^r - (j + 1 + x)^r\bigr)\) (principal powers) has sum \(f(r, x)\) and also has sum \(g(r, x)\). Then \(f(r, x) = g(r, x)\) for every admissible \(x\) and every complex \(r\), and for every natural number \(m\) and every admissible \(x\), \(f(m, x) = g(m, x) = \bigl(B_{m+1}(x + 1) - B_{m+1}(1)\bigr)/(m + 1)\), where \(B_n\) is the \(n\)-th Bernoulli polynomial.

theorem ramanujan_part1_ch7_entry9_zetaeven
    (phi psi : ℂ → ℂ → ℂ)
    (hphi_entire : ∀ x, chapter7Admissible x →
      Differentiable ℂ (fun r : ℂ => phi r x))
    (hpsi_entire : ∀ x, chapter7Admissible x →
      Differentiable ℂ (fun r : ℂ => psi r x))
    (hphi_series : ∀ r x, r.re < 0 → chapter7Admissible x →
      HasSum (chapter7PowerDifferenceTerm r x) (phi r x))
    (hpsi_series : ∀ r x, r.re < 0 → chapter7Admissible x →
      HasSum (chapter7PowerDifferenceTerm r x) (psi r x)) :
    (∀ x, chapter7Admissible x → ∀ r, phi r x = psi r x) ∧
      (∀ m : ℕ, ∀ x, chapter7Admissible x →
        phi m x = chapter7IntegerPhi m x ∧
          psi m x = chapter7IntegerPhi m x)

Sources

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

Uses 3

Statement usesBernoulli-polynomial form of Berndt's \(\varphi_r\) · Admissible parameters for the power-difference series · Terms of the power-difference series

33 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.