Email Gateway (Nov 01 2024 at 15:20): Email Gateway (Nov 01 2024 at 15:20):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce yet another big contribution by the ever-prolific Manuel Eberl:
The Boustrophedon Transform, the Entringer Numbers, and Related Sequences
This entry defines the Boustrophedon transform, which can be seen as either a transformation of a sequence of numbers or, equivalently, an exponential generating function. We define it in terms of the Seidel triangle, a number triangle similar to Pascal's triangle, and then prove the closed form B(f) = (sec+tan)f.
We also define several related sequences, such as:
Reasonably efficient executable algorithms to compute the Boustrophedon transform and related sequences are also given, using Imperative HOL.
Online at https://www.isa-afp.org/entries/Boustrophedon_Transform.html
Larry
Last updated: Jan 04 2025 at 20:18 UTC