Re: [isabelle] Discrete Summation

For an example in my PhD I formalized Stirling numbers of the first and
second kind (more about 2nd kind) and the main theorem that transforms
normal powers as sums of falling powers with stirling numbers (2nd
kind). There is also a simple part about forward differentiation and
those operators you need for discrete summation. Basic stuff, no
hypergeometric summation and the like. Of course in the drawer... I'll
send it over.

Best wishes,


Florian Haftmann wrote:

> Hi out there,
> here at TUM we plan to start a student project formalizing factorial
> chains, Stirling numbers, discrete summation and related stuff, which
> seems yet underrepresented in the formal area, at least according to
> Google and the Isabelle repositories.  However, to avoid work in
> parallel, I would like to ask whether somebody out there is working in
> that direction or has some related stuff in the drawer.
> Any feedback welcome,
>     Florian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.