Discretisations of higher order and the theorems of Faa di Bruno and DeMoivre-Laplace

IMME VAN DEN BERG

We formalize Definition 7.3.

def B (ν : ℕ) (j : ℕ) : ℚ

Equations

• B ν j = ↑(ν.choose j) * (1 / 2) ^ ν