Diff — Recurrence relation

Revision #2831 → #3302 · back to history

addedFibonacci sequence2c2db0278596

addedGenerating function of the Fibonacci sequence761295cb55f8

modifiedk-th differenceb96666c533ab

Field	From #2831	To #3302
mathlib.decl	fwdDiff	fwdDiff_iter_eq_sum_shift
note	The k-th difference appears as `Function.iterate (fwdDiff h) k` in lemmas but is not separately defined.	The k-th difference appears as `Function.iterate (fwdDiff h) k`; `fwdDiff_iter_eq_sum_shift` gives its binomial expansion.

addedBessel function as solution of a linear recurrence4b6eabf23419

addedConfluent hypergeometric series as solution of a linear recurrencea0ca8901dcce