English
The nth forward difference of f is given by a sum of shifted values of f with binomial coefficients.
Русский
n-я передняя разность f выражается через сумму значений f в сдвинутых аргументах с биномальными коэффициентами.
LaTeX
$$$ Δ_h^{[n]} f(y) = \sum_{k=0}^{n} (-1)^{n-k} {n \choose k} f(y + k h) $$$
Lean4
/-- **Gregory-Newton formula** expressing `f (y + n • h)` in terms of the iterated forward differences
of `f` at `y`.
-/
theorem shift_eq_sum_fwdDiff_iter (f : M → G) (n : ℕ) (y : M) :
f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y :=
by
convert congr_fun (LinearMap.congr_fun ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1
· rw [← shiftₗ_pow_apply h f, shiftₗ]
· simp [Module.End.pow_apply, coe_fwdDiffₗ]
