Differences of powers

Stream: Is there code for X?

[Martin Dvořák]

Do we have this thing in Mathlib?
differences.png
You will probably recognize this pattern (which works for any exponent) faster from a picture.

[Jireh Loreaux]

Are you asking if we have discrete calculus?

[Martin Dvořák]

I had no idea it had a name!

[Jireh Loreaux]

(Maybe I got the name wrong, hold on)

[Martin Dvořák]

BTW this code generated those numbers (no proof included):

def apply_repeatedly {α : Type} (op : α → α) (x : α) : Nat → α
| 0   => x
| n+1 => apply_repeatedly op (op x) n

def diffs : List Nat → List Nat
| [ ]         => []
| [ _ ]       => []
| a :: b :: l => (b-a) :: diffs (b :: l)

def magic (n : Nat) : List Nat :=
  apply_repeatedly diffs (List.map (· ^ n) (List.range 10)) n

#eval magic 2
#eval magic 3
#eval magic 4
#eval magic 5
#eval magic 6

[Jireh Loreaux]

A nice introduction to this is here: https://homepages.math.uic.edu/~kauffman/DCalc.pdf, and it assumes almost no background knowledge. The wikipedia page can get a bit heady in places.

[Yaël Dillies]

I have some code in a lost branch of mathlib. Tell me what you want more precisely and I might have it.

[Martin Dvořák]

Do we have a proof that the nth column is n! all the way?

[Yaël Dillies]

Oh that's easy.

[Yaël Dillies]

I have the result that the leading coeff of the discrete difference of a polynomial is its leading coeff times its degree. Then you induct and tada.

[Martin Dvořák]

Perfect! May I get a link to your result? I would love to do the corollary with my students by the end of our course.

[Alex Kontorovich]

Jireh Loreaux said:

A nice introduction to this is here: https://homepages.math.uic.edu/~kauffman/DCalc.pdf, and it assumes almost no background knowledge. The wikipedia page can get a bit heady in places.

I learned this from Conway, who called it "Bernouilli calculus": https://twitter.com/AlexKontorovich/status/1075779916480811010?s=20 (The joke of course is that Bernouilli was doing the continuous calculus, too!...)