Theorems · Theorem · difference equations

shift_eq_sum_fwdDiff_iter

∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : 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.

Defined in

Mathlib.Algebra.Group.ForwardDiff

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidAddCommGroup