Inverting shift and difference operators

TheoremRamanujan's operator identity for the Bernoulli numbers#✓fully proved

For a sequence \(a = (a_n)_{n \ge 0}\) of real numbers, a real number \(h\) and a real polynomial \(\varphi\) of degree \(d\) (with \(d = 0\) for \(\varphi = 0\)), let \(S_a(h, \varphi) = \sum_{n=0}^{d} a_n h^n \varphi^{(n)}\). Let \(b_n = B_n / n!\), where \(B_n\) are the Bernoulli numbers with \(B_1 = -\tfrac12\). Then for every real polynomial \(\varphi\) and every real \(h\), \(S_b(h, \varphi)(x + h) - S_b(h, \varphi)(x) = h \varphi'(x)\) as polynomials in \(x\). Moreover \(b\) is the only such sequence: if a real sequence \(a\) satisfies \(S_a(h, \varphi)(x + h) - S_a(h, \varphi)(x) = h \varphi'(x)\) for every real polynomial \(\varphi\) and every real \(h\), then \(a_n = b_n\) for every \(n\).

theorem ramanujan_part1_ch5_entry1 :
    (∀ (phi : ℝ[X]) (h : ℝ),
      Polynomial.taylor h
          (chapter5DerivativeExpansion chapter5Entry1MinusCoeff h phi) -
        chapter5DerivativeExpansion chapter5Entry1MinusCoeff h phi =
      Polynomial.C h * phi.derivative) ∧
    ∀ a : ℕ → ℝ,
      (∀ (phi : ℝ[X]) (h : ℝ),
        Polynomial.taylor h (chapter5DerivativeExpansion a h phi) -
            chapter5DerivativeExpansion a h phi =
          Polynomial.C h * phi.derivative) →
      a = chapter5Entry1MinusCoeff

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5. The source's shift p(x) ↦ p(x + h) is Polynomial.taylor h, and the operator ∑ aₙ hⁿ Dⁿ is Entry1Euleriangf.chapter5DerivativeExpansion.

DefinitionPolynomial shift#✓fully proved

For a semiring \(R\), an element \(h \in R\) and a polynomial \(p \in R[x]\), the shift of \(p\) by \(h\) is the polynomial \(p(x + h)\), the composition of \(p\) with \(x + h\).

def chapter5PolynomialShift {R : Type*} [Semiring R]
    (h : R) (p : R[X]) : R[X] :=
  p.comp (Polynomial.X + Polynomial.C h)

Used by 1

Used byRamanujan's operator identity for \((1 - 2^n) B_n / n!\)

TheoremRamanujan's operator identity for \((1 - 2^n) B_n / n!\)#✓fully proved

For a sequence \(a = (a_n)_{n \ge 0}\) of real numbers, a real number \(h\) and a real polynomial \(\varphi\) of degree \(d\) (with \(d = 0\) for \(\varphi = 0\)), let \(S_a(h, \varphi) = \sum_{n=0}^{d} a_n h^n \varphi^{(n)}\). Let \(c_n = (1 - 2^n) B_n / n!\), where \(B_n\) are the Bernoulli numbers with \(B_1 = -\tfrac12\). Then for every real polynomial \(\varphi\) and every real \(h\), \(S_c(h, \varphi)(x + h) + S_c(h, \varphi)(x) = h \varphi'(x)\) as polynomials in \(x\). Moreover \(c\) is the only such sequence: if a real sequence \(a\) satisfies \(S_a(h, \varphi)(x + h) + S_a(h, \varphi)(x) = h \varphi'(x)\) for every real polynomial \(\varphi\) and every real \(h\), then \(a_n = c_n\) for every \(n\).

theorem ramanujan_part1_ch5_entry1_euleriangf :
    (∀ (phi : ℝ[X]) (h : ℝ),
      chapter5PolynomialShift h
          (chapter5DerivativeExpansion chapter5Entry1PlusCoeff h phi) +
        chapter5DerivativeExpansion chapter5Entry1PlusCoeff h phi =
      Polynomial.C h * phi.derivative) ∧
    ∀ a : ℕ → ℝ,
      (∀ (phi : ℝ[X]) (h : ℝ),
        chapter5PolynomialShift h (chapter5DerivativeExpansion a h phi) +
            chapter5DerivativeExpansion a h phi =
          Polynomial.C h * phi.derivative) →
      a = chapter5Entry1PlusCoeff

Sources

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

Uses 1

Statement usesPolynomial shift

TheoremThe polynomial shift is the Taylor shift#✓fully proved

For a semiring \(R\), an element \(h \in R\) and a polynomial \(p \in R[x]\), the shift \(p(x + h)\) (the composition of \(p\) with \(x + h\)) equals the Taylor expansion of \(p\) at \(h\), the polynomial whose coefficient of \(x^k\) is the \(k\)-th Hasse derivative of \(p\) evaluated at \(h\).

theorem chapter5PolynomialShift_eq_taylor {R : Type*} [Semiring R] (h : R) (p : R[X]) :
    chapter5PolynomialShift h p = Polynomial.taylor h p

TheoremRamanujan's solutions of two central difference equations#✓fully proved

Let \(\varphi\) be a real polynomial of degree \(d\) (with \(d = 0\) for \(\varphi = 0\)). For \(n \ge 0\) let \(F_n(x) = \varphi(x) + \sum_{k=1}^{n} \frac{(-1)^k (n!)^2}{(n+k)!\,(n-k)!} \bigl(\varphi(x+k) + \varphi(x-k)\bigr)\), and let \(M = \sum_{n=0}^{\lfloor d/2 \rfloor} \frac{1}{2n+1} F_n\) and \(P = \sum_{n=0}^{\lfloor d/2 \rfloor} \binom{2n}{n} 2^{-n} F_n\). Then \(F_n = 0\) for every \(n\) with \(d < 2n\), \(M(x+1) - M(x-1) = 2 \varphi'(x)\) and \(P(x+1) + P(x-1) = 2 \varphi(x)\), as polynomials in \(x\).

theorem ramanujan_part1_ch5_entry2i_euleriangf (phi : ℝ[X]) :
    (∀ n : ℕ, phi.natDegree < 2 * n → chapter5Entry2F phi n = 0) ∧
      chapter5PolynomialShift 1 (chapter5Entry2MinusSolution phi) -
          chapter5PolynomialShift (-1) (chapter5Entry2MinusSolution phi) =
        Polynomial.C 2 * phi.derivative ∧
      chapter5PolynomialShift 1 (chapter5Entry2PlusSolution phi) +
          chapter5PolynomialShift (-1) (chapter5Entry2PlusSolution phi) =
        Polynomial.C 2 * phi

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5, Entry 2(i), pp. 111–112.

TheoremEulerian-polynomial inverse of a shift-plus-multiple operator#✓fully proved

Let \(A(n, k)\) be the Eulerian numbers, given by \(A(0, 0) = 1\), \(A(0, k) = 0\) for \(k \ge 1\) and \(A(n + 1, k) = (k + 1) A(n, k) + (n + 1 - k) A(n, k - 1)\), the last term read as \(0\) when \(k = 0\). For \(p \in \mathbb{C}\) set \(\psi_0(p) = 1\) and \(\psi_n(p) = \sum_{k=0}^{n-1} A(n, k) (-p)^k\) for \(n \ge 1\). For a sequence \(a_0, a_1, \ldots\) of complex numbers, \(h \in \mathbb{C}\) and a polynomial \(\varphi \in \mathbb{C}[x]\), write \(E_{a,h} \varphi = \sum_{n=0}^{\deg \varphi} a_n h^n \varphi^{(n)}\), where \(\varphi^{(n)}\) is the \(n\)-th derivative. Fix \(p \in \mathbb{C}\) with \(p \ne -1\) and put \(c_n = \frac{(-1)^n \psi_n(p)}{n! \, (p + 1)^{n + 1}}\). Then: (1) for every \(h \in \mathbb{C}\) and every \(\varphi \in \mathbb{C}[x]\), the polynomial \(f = E_{c,h} \varphi\) satisfies \(f(x + h) + p f(x) = \varphi(x)\) as polynomials in \(x\); (2) if a sequence \(a\) of complex numbers is such that \(f = E_{a,h} \varphi\) satisfies \(f(x + h) + p f(x) = \varphi(x)\) for every \(h \in \mathbb{C}\) and every \(\varphi \in \mathbb{C}[x]\), then \(a_n = c_n\) for every \(n \ge 0\).

theorem ramanujan_part1_ch5_entry3 (p : ℂ) (hp : p ≠ -1) :
    (∀ (h : ℂ) (phi : Polynomial ℂ),
      Polynomial.taylor h
            (chapter5DerivativeExpansion (fun n => chapter5Entry3Coeff n p) h phi) +
          Polynomial.C p *
            chapter5DerivativeExpansion (fun n => chapter5Entry3Coeff n p) h phi =
        phi) ∧
      ∀ a : ℕ → ℂ,
        (∀ (h : ℂ) (phi : Polynomial ℂ),
          Polynomial.taylor h (chapter5DerivativeExpansion a h phi) +
              Polynomial.C p * chapter5DerivativeExpansion a h phi =
            phi) →
        ∀ n : ℕ, a n = chapter5Entry3Coeff n p

Sources

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

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.