Documentation

TauCeti.Algebra.Group.ForwardDiff

Alternating forward differences and the discrete Leibniz rule #

For functions from an additive commutative monoid to an additive commutative group, multiplying the n-th forward difference by the integer (-1) ^ n gives the alternating difference. These identities describe its successor step and its alternating binomial expansion, using Mathlib's forward-difference operator and integer scalar multiplication. For ring-valued functions, the same identities are stated using multiplication by the coefficients in the ring.

The discrete Leibniz rule computes differences of a scalar product from finitely many differences of its factors. Its shifted form evaluates the second factor along the arithmetic progression starting at the input point. Its unshifted form uses only differences at that point, of orders at most the output order, so it also computes products in finite-difference coordinates.

The k-th forward difference of t ↦ t ^ m at 0 is k! S(m, k), where S is the Stirling number of the second kind. Expanding (x + i h) ^ m binomially then writes the k-th forward difference of y ↦ y ^ m with any step h at any point x as k! times an integral combination of the monomials x ^ (m - l) h ^ l, k ≤ l ≤ m. This explicit divisibility by k! is what bounds forward differences of power series over ultrametric rings.

Main declarations #

source
theorem TauCeti.neg_one_pow_smul_fwdDiff_iter_succ {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (n : ℕ) (F : M → G) (s : M) :
(-1) ^ n • (fwdDiff s)^[n] (-fwdDiff s F) = (-1) ^ (n + 1) • (fwdDiff s)^[n + 1] F

Differencing once advances the alternating iterated forward difference by one step.

source
theorem TauCeti.neg_one_pow_smul_fwdDiff_iter_eq_alternating_sum {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (n : ℕ) (F : M → G) (s x : M) :
(-1) ^ n • (fwdDiff s)^[n] F x = ∑ k ∈ Finset.range (n + 1), ((-1) ^ k * ↑(n.choose k)) • F (x + k • s)

The alternating iterated forward difference as an explicit alternating binomial sum.

source
theorem TauCeti.neg_one_pow_mul_fwdDiff_iter_succ {M : Type u_1} [AddCommMonoid M] {R : Type u_3} [Ring R] (n : ℕ) (F : M → R) (s : M) :
(fun (x : M) => (-1) ^ n * (fwdDiff s)^[n] (-fwdDiff s F) x) = fun (x : M) => (-1) ^ (n + 1) * (fwdDiff s)^[n + 1] F x

Differencing once advances the alternating iterated forward difference of a ring-valued function by one step.

source
theorem TauCeti.neg_one_pow_mul_fwdDiff_iter_eq_alternating_sum {M : Type u_1} [AddCommMonoid M] {R : Type u_3} [Ring R] (n : ℕ) (F : M → R) (s x : M) :
(-1) ^ n * (fwdDiff s)^[n] F x = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * F (x + k • s)

The alternating iterated forward difference of a ring-valued function as an explicit alternating binomial sum.

source
theorem TauCeti.sum_neg_one_pow_mul_choose_succ {R : Type u_3} [Ring R] (n : ℕ) (f : ℕ → R) :
∑ k ∈ Finset.range (n + 2), (-1) ^ k * ↑((n + 1).choose k) * f k = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (f k - f (k + 1))

An alternating binomial sum of successor order is the alternating binomial sum of the negative forward differences of consecutive values.

source
theorem TauCeti.fwdDiff_iter_smul {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {R : Type u_3} [Ring R] [Module R G] (h : M) (f : M → R) (g : M → G) (n : ℕ) :
(fwdDiff h)^[n] (f • g) = fun (x : M) => ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • (fwdDiff h)^[ij.1] f x • (fwdDiff h)^[ij.2] g (x + ij.1 • h)

Discrete Leibniz rule. The n-th difference of a scalar product is a binomial sum of products of differences. In the term with orders i and j, the second factor is evaluated at x + i • h, where i + j = n. No commutativity of the scalar ring is required.

source
theorem TauCeti.fwdDiff_iter_smul_eq_sum_range {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {R : Type u_3} [Ring R] [Module R G] (h : M) (f : M → R) (g : M → G) (n : ℕ) (x : M) :
(fwdDiff h)^[n] (f • g) x = ∑ i ∈ Finset.range (n + 1), n.choose i • (fwdDiff h)^[i] f x • (fwdDiff h)^[n - i] g (x + i • h)

Range-indexed discrete Leibniz rule for a scalar product.

source
theorem TauCeti.fwdDiff_iter_smul_eq_sum_range_sum_range {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {R : Type u_3} [Ring R] [Module R G] (h : M) (f : M → R) (g : M → G) (n : ℕ) (x : M) :
(fwdDiff h)^[n] (f • g) x = ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (i + 1), (n.choose i * i.choose j) • (fwdDiff h)^[i] f x • (fwdDiff h)^[n - i + j] g x

Unshifted discrete Leibniz rule. Expanding the shifted differences in the discrete Leibniz rule by the Gregory–Newton formula expresses the result using differences at x only. In particular, only orders at most n of each input occur.

source
theorem TauCeti.fwdDiff_iter_pow_apply_zero {R : Type u_4} [Ring R] (k m : ℕ) :
(fwdDiff 1)^[k] (fun (t : R) => t ^ m) 0 = ↑k.factorial * ↑(m.stirlingSecond k)

Forward differences of powers at zero. The k-th forward difference of t ↦ t ^ m at 0 is k! times the Stirling number of the second kind S(m, k). In particular it vanishes for m < k and equals k! for m = k (fwdDiff_iter_eq_factorial).

source
theorem TauCeti.fwdDiff_iter_pow_eq_sum {R : Type u_4} [CommRing R] (h x : R) (k m : ℕ) :
(fwdDiff h)^[k] (fun (y : R) => y ^ m) x = ∑ l ∈ Finset.range (m + 1), x ^ (m - l) * h ^ l * ↑(m.choose l) * (↑k.factorial * ↑(l.stirlingSecond k))

Forward differences of powers with any step. The k-th forward difference of y ↦ y ^ m with step h at x is ∑ₗ C(m, l) x ^ (m - l) h ^ l k! S(l, k), where S is the Stirling number of the second kind. Only the terms with k ≤ l are nonzero, and every term is divisible by k!.