Forward difference operators and Newton series

We define the forward difference operator, sending f to the function x ↦ f (x + h) - f x for a given h (for any additive semigroup, taking values in an abelian group). The notation Δ_[h] is defined for this operator, scoped in namespace fwdDiff.

We prove two key formulae about this operator:

• shift_eq_sum_fwdDiff_iter: the Gregory-Newton formula, expressing f (y + n • h) as a linear combination of forward differences of f at y, for n ∈ ℕ;
• fwdDiff_iter_eq_sum_shift: formula expressing the n-th forward difference of f at y as a linear combination of f (y + k • h) for 0 ≤ k ≤ n.

We also prove some auxiliary results about iterated forward differences of the function n ↦ n.choose k.

def fwdDiff {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) : M → G

Forward difference operator, fwdDiff h f n = f (n + h) - f n. The notation Δ_[h] for this operator is available in the fwdDiff namespace.

Equations

• fwdDiff h f n = f (n + h) - f n

def fwdDiff.«termΔ_[_]» : Lean.ParserDescr

Forward difference operator, fwdDiff h f n = f (n + h) - f n. The notation Δ_[h] for this operator is available in the fwdDiff namespace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem fwdDiff_add {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f g : M → G) : fwdDiff h (f + g) = fwdDiff h f + fwdDiff h g

@[simp]

theorem fwdDiff_const {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (g : G) : (fwdDiff h fun (x : M) => g) = fun (x : M) => 0

theorem fwdDiff_smul {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) {R : Type} [Ring R] [Module R G] (f : M → R) (g : M → G) : fwdDiff h (f • g) = fwdDiff h f • g + f • fwdDiff h g + fwdDiff h f • fwdDiff h g

@[simp]

theorem fwdDiff_const_smul {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) {R : Type u_3} [Monoid R] [DistribMulAction R G] (r : R) (f : M → G) : fwdDiff h (r • f) = r • fwdDiff h f

@[simp]

theorem fwdDiff_smul_const {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) {R : Type} [Ring R] [Module R G] (f : M → R) (g : G) : (fwdDiff h fun (y : M) => f y • g) = fwdDiff h f • fun (x : M) => g

Forward-difference and shift operators as linear endomorphisms

This section contains versions of the forward-difference operator and the shift operator bundled as ℤ-linear endomorphisms. These are useful for certain proofs; but they are slightly annoying to use, as the source and target types of the maps have to be specified each time, and various coercions need to be un-wound when the operators are applied, so we also provide the un-bundled version.

def fwdDiff_aux.fwdDiffₗ (M : Type u_1) (G : Type u_2) [AddCommMonoid M] [AddCommGroup G] (h : M) : Module.End ℤ (M → G)

Linear-endomorphism version of the forward difference operator.

Equations

• fwdDiff_aux.fwdDiffₗ M G h = { toFun := fwdDiff h, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem fwdDiff_aux.fwdDiffₗ_apply (M : Type u_1) (G : Type u_2) [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (a✝ : M) : (fwdDiffₗ M G h) f a✝ = fwdDiff h f a✝

theorem fwdDiff_aux.coe_fwdDiffₗ {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) : ⇑(fwdDiffₗ M G h) = fwdDiff h

theorem fwdDiff_aux.coe_fwdDiffₗ_pow {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (n : ℕ) : ⇑(fwdDiffₗ M G h ^ n) = (fwdDiff h)^[n]

def fwdDiff_aux.shiftₗ (M : Type u_1) (G : Type u_2) [AddCommMonoid M] [AddCommGroup G] (h : M) : Module.End ℤ (M → G)

Linear-endomorphism version of the shift-by-1 operator.

Equations

• fwdDiff_aux.shiftₗ M G h = fwdDiff_aux.fwdDiffₗ M G h + 1

theorem fwdDiff_aux.shiftₗ_apply {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (y : M) : (shiftₗ M G h) f y = f (y + h)

theorem fwdDiff_aux.shiftₗ_pow_apply {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (k : ℕ) (y : M) : (shiftₗ M G h ^ k) f y = f (y + k • h)

@[simp]

theorem fwdDiff_finset_sum {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) {α : Type u_3} (s : Finset α) (f : α → M → G) : fwdDiff h (∑ k ∈ s, f k) = ∑ k ∈ s, fwdDiff h (f k)

@[simp]

theorem fwdDiff_iter_add {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f g : M → G) (n : ℕ) : (fwdDiff h)^[n] (f + g) = (fwdDiff h)^[n] f + (fwdDiff h)^[n] g

@[simp]

theorem fwdDiff_iter_const_smul {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) {R : Type u_3} [Monoid R] [DistribMulAction R G] (r : R) (f : M → G) (n : ℕ) : (fwdDiff h)^[n] (r • f) = r • (fwdDiff h)^[n] f

@[simp]

theorem fwdDiff_iter_finset_sum {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) {α : Type u_3} (s : Finset α) (f : α → M → G) (n : ℕ) : (fwdDiff h)^[n] (∑ k ∈ s, f k) = ∑ k ∈ s, (fwdDiff h)^[n] (f k)

theorem fwdDiff_iter_eq_sum_shift {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (n : ℕ) (y : M) : (fwdDiff h)^[n] f y = ∑ k ∈ Finset.range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Express the n-th forward difference of f at y in terms of the values f (y + k), for 0 ≤ k ≤ n.

theorem fwdDiff_iter_comp_add {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (m : M) (n : ℕ) (y : M) : (fwdDiff h)^[n] (fun (r : M) => f (r + m)) y = (fwdDiff h)^[n] f (y + m)

theorem fwdDiff_comp_add {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (m y : M) : fwdDiff h (fun (r : M) => f (r + m)) y = fwdDiff h f (y + m)

theorem shift_eq_sum_fwdDiff_iter {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (n : ℕ) (y : M) : f (y + n • h) = ∑ k ∈ Finset.range (n + 1), n.choose k • (fwdDiff h)^[k] f y

Gregory-Newton formula expressing f (y + n • h) in terms of the iterated forward differences of f at y.

theorem fwdDiff_choose (j : ℕ) : (fwdDiff 1 fun (x : ℕ) => ↑(x.choose (j + 1))) = fun (x : ℕ) => ↑(x.choose j)

theorem fwdDiff_iter_choose (j k : ℕ) : ((fwdDiff 1)^[k] fun (x : ℕ) => ↑(x.choose (k + j))) = fun (x : ℕ) => ↑(x.choose j)

theorem fwdDiff_iter_choose_zero (m n : ℕ) : (fwdDiff 1)^[n] (fun (x : ℕ) => ↑(x.choose m)) 0 = if n = m then 1 else 0

theorem fwdDiff_addChar_eq {M : Type u_3} {R : Type u_4} [AddCommMonoid M] [Ring R] (φ : AddChar M R) (x h : M) (n : ℕ) : (fwdDiff h)^[n] (⇑φ) x = (φ h - 1) ^ n * φ x

Forward differences of polynomials

We prove formulae about the forward difference operator applied to polynomials:

• fwdDiff_iter_pow_eq_zero_of_lt : The n-th forward difference of the function x ↦ x^j is zero if j < n;
• fwdDiff_iter_eq_factorial : The n-th forward difference of the function x ↦ x^n is the constant function n!;
• fwdDiff_iter_sum_mul_pow_eq_zero : The n-th forward difference of a polynomial of degree < n is zero (formulated using explicit sums over range n).

theorem fwdDiff_iter_pow_eq_zero_of_lt {R : Type u_3} [CommRing R] {j n : ℕ} (h : j < n) : ((fwdDiff 1)^[n] fun (r : R) => r ^ j) = 0

The n-th forward difference of the function x ↦ x^j is zero if j < n.

theorem fwdDiff_iter_eq_factorial {R : Type u_3} [CommRing R] {n : ℕ} : ((fwdDiff 1)^[n] fun (r : R) => r ^ n) = ↑n.factorial

The n-th forward difference of x ↦ x^n is the constant function n!.

theorem Polynomial.fwdDiff_iter_degree_eq_factorial {R : Type u_3} [CommRing R] (P : Polynomial R) : ((fwdDiff 1)^[P.natDegree] fun (x : R) => eval x P) = P.leadingCoeff • ↑P.natDegree.factorial

theorem Polynomial.fwdDiff_iter_eq_zero_of_degree_lt {R : Type u_3} [CommRing R] {P : Polynomial R} {n : ℕ} (hP : P.natDegree < n) : ((fwdDiff 1)^[n] fun (x : R) => eval x P) = 0

theorem Polynomial.fwdDiff_iter_degree_add_one_eq_zero {R : Type u_3} [CommRing R] (P : Polynomial R) : ((fwdDiff 1)^[P.natDegree + 1] fun (x : R) => eval x P) = 0

theorem fwdDiff_iter_sum_mul_pow_eq_zero {R : Type u_3} [CommRing R] {n : ℕ} (P : ℕ → R) : ((fwdDiff 1)^[n] fun (r : R) => ∑ k ∈ Finset.range n, P k * r ^ k) = 0

The n-th forward difference of a polynomial of degree < n is zero (formulated using explicit sums over range n).