Commit 2024-11-13 20:45 0e1492de

View on Github →

feat(Algebra/Group): forward difference operator (#17699) We define the forward-difference (discrete derivative) operator, and prove the Gregory-Newton formula (discrete version of Taylor's theorem). Based on results from the ETH bachelor thesis of Giulio Caflisch.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/ForwardDiff.lean

added def fwdDiff

added theorem fwdDiff_add

added theorem fwdDiff_aux.coe_fwdDiffₗ

added theorem fwdDiff_aux.coe_fwdDiffₗ_pow

added def fwdDiff_aux.fwdDiffₗ

added def fwdDiff_aux.shiftₗ

added theorem fwdDiff_aux.shiftₗ_apply

added theorem fwdDiff_aux.shiftₗ_pow_apply

added theorem fwdDiff_choose

added theorem fwdDiff_const

added theorem fwdDiff_const_smul

added theorem fwdDiff_finset_sum

added theorem fwdDiff_iter_add

added theorem fwdDiff_iter_choose

added theorem fwdDiff_iter_choose_zero

added theorem fwdDiff_iter_const_smul

added theorem fwdDiff_iter_eq_sum_shift

added theorem fwdDiff_iter_finset_sum

added theorem fwdDiff_smul

added theorem fwdDiff_smul_const

added theorem shift_eq_sum_fwdDiff_iter