English
Express the original function value f(y + n h) in terms of iterated forward differences at y: f(y + n h) = ∑_{k=0}^{n} binom(n,k) · Δ_h^[k] f(y).
Русский
Выражаем f(y + n h) через итеративные прямые разности в точке y: f(y + n h) = ∑_{k=0}^{n} {n \choose k} · Δ_h^[k] f(y).
LaTeX
$$$ f(y + n h) = \sum_{k=0}^{n} {n \choose k} \cdot Δ_h^{[k]} f y $$$
Lean4
/-- 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_eq_sum_shift (f : M → G) (n : ℕ) (y : M) :
Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), ((-1 : ℤ) ^ (n - k) * n.choose k) • f (y + k • h) := by
-- rewrite in terms of `(shiftₗ - 1) ^ n`
have : fwdDiffₗ M G h = shiftₗ M G h - 1 := by simp only [shiftₗ, add_sub_cancel_right]
rw [← coe_fwdDiffₗ, this, ← Module.End.pow_apply]
-- use binomial theorem `Commute.add_pow` to expand this
have : Commute (shiftₗ M G h) (-1) := (Commute.one_right _).neg_right
convert congr_fun (LinearMap.congr_fun (this.add_pow n) f) y using 3
· simp only [sub_eq_add_neg]
· rw [LinearMap.sum_apply, sum_apply]
congr 1 with k
have : ((-1) ^ (n - k) * n.choose k : Module.End ℤ (M → G)) = ↑((-1) ^ (n - k) * n.choose k : ℤ) := by norm_cast
rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, LinearMap.map_smul, Pi.smul_apply,
shiftₗ_pow_apply]
