Newton sequences

DefinitionNewton sequences#✓fully proved

Let \(R\) be a commutative semiring and let \(a, c \colon \mathbb{N} \to R\). The sequence \(a\) is a Newton sequence generated by \(c\) if for every natural number \(n\), \(a_{n+1} = \sum_{j=0}^{n-1} a_{n-j} c_{j+1} + (n+1) c_{n+1}\).

Equivalently, \(a_m = \sum_{k=1}^{m-1} a_{m-k} c_k + m c_m\) for every \(m \ge 1\). The sequences in the sources begin at index one, so \(a_0\) and \(c_0\) play no role. The two sources write the factors in opposite orders, which agree because \(R\) is commutative.

def IsNewtonSequence {R : Type*} [CommSemiring R] (a c : ℕ → R) : Prop :=
  ∀ n : ℕ,
    a (n + 1) =
      (∑ j ∈ Finset.range n, a (n - j) * c (j + 1)) + ((n + 1 : ℕ) : R) * c (n + 1)

Sources

• JIS VOL18/Wojcik, https://cs.uwaterloo.ca/journals/JIS/VOL18/Wojcik/wojcik6.tex, lines 276–280; JIS VOL8/Huang, https://cs.uwaterloo.ca/journals/JIS/VOL8/Huang/huang11.tex, lines 176–179.

Used by 1

Used byThe recurrence of a Newton sequence

TheoremThe recurrence of a Newton sequence#✓fully proved

Let \(R\) be a commutative semiring and let \(a, c \colon \mathbb{N} \to R\) be such that \(a\) is a Newton sequence generated by \(c\). Then for every natural number \(n\) we have \(a_{n+1} = \sum_{j=0}^{n-1} a_{n-j} c_{j+1} + (n+1) c_{n+1}\).

theorem IsNewtonSequence.eq_recurrence {R : Type*} [CommSemiring R]
    {a c : ℕ → R} (h : IsNewtonSequence a c) (n : ℕ) :
    a (n + 1) =
      (∑ j ∈ Finset.range n, a (n - j) * c (j + 1)) + ((n + 1 : ℕ) : R) * c (n + 1)

Uses 1

Statement usesNewton sequences

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.