Email Gateway (Aug 22 2022 at 15:07): Email Gateway (Aug 22 2022 at 15:07):From: Raymond Rogers <raymond.rogers72@gmail.com>
I am a complete newbie to Isabelle.
I am trying to implement a library that is capable, more or less, of
validating some of Gould's identities. In particular the ones listed in:
http://www.dsi.dsi.unifi.it/~resp/GouldBK.pdf
I have managed "verify" the first equation "BS"
lemma Isa_BS:
assumes kn: "m ≤ n"
shows "(n choose m) = (n choose (n-m))"
using assms
apply (rule Binomial.binomial_symmetric)
done
(suggestions appreciated!!)
I wish to extend/expand/define the choose function to
(n choose m) to n negative.
This is the second item in GouldBK.pdf
and in
Riordan's "Introduction to Combinatorial Analysis" page 5
and elsewhere
My question is strategic. Should I just introduce a new "type" and
filter the input into Binomial.thy or go through the whole definition
phase copying (or something) Binomial.thy. Possibly there is a way to
use "gbinomial" but I am not there yet. Or use the normal field
extension process somehow? Using (a,b) over a; and defining
multiplication and addition.
Is there a tutorial with examples using Binomial.thy (and the fps
theory)? There seems to be some peculiarities using "=" instead of
"-->" but that is probably just ignorance.
Ray
Email Gateway (Aug 22 2022 at 15:07):From: Manuel Eberl <eberlm@in.tum.de>
gbinomial (syntax: "n gchoose k") is already that generalisation. It
works for pretty much anything as the first argument, but the second
argument must be a natural numbers. Seeing as we have the Gamma and Beta
functions in HOL-Analysis, one could also easily extend it to complex
numbers.
I'm not sure what field extensions have to do with any of this. What
field are you talking about? What do you want to extend it to? What does
that have to do with binomial coefficients?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:08):From: Lawrence Paulson <lp15@cam.ac.uk>
You simply need to use gchoose. Example:
value "(-1/2::real) gchoose 2"
"3 / 8"
:: “real"
The first argument has to be a field of characteristic zero, such as the reels.
Larry
Email Gateway (Aug 22 2022 at 15:08):From: Raymond Rogers <raymond.rogers72@gmail.com>
Thanks! Is there readable reference material for these lemma's?
Normally in mathematics one is expected to provide
references/bibliography. In my experience self-documenting code ends
up being a little painful.
Ray
"
Email Gateway (Aug 22 2022 at 15:08):From: Lawrence Paulson <lp15@cam.ac.uk>
I agree with you that reference material is highly desirable, but unfortunately very few of our proofs are currently linked to sources.
Larry Paulson
Email Gateway (Aug 22 2022 at 15:08):From: Raymond Rogers <raymond.rogers72@gmail.com>
Thanks: I want to twist some of the results in Gouldbk.pdf and want to
see how robust the basic results are and check if my conclusions are
correct usages. Some of the techniques in the paper are long and not
too obvious (to me).
Perhaps my use of "field extension" was inappropriate.
My intuition is that if you are lacking something that is reasonable you
can extend a base set a by (a,b) and form a new set. For instance:
adding negative numbers to the naturals,
creating fractions from integers
solutions to x^2-2=0
and of course "imaginary numbers"
Of course you have to prove consistency and such.
The procedures seem fairly standard at an intuitive level.
Is there a standard template/example/constructor in Isabelle for this
sort of thing? So a construct can be introduced and checked for
consistency.
For binomials: I could imagine (a choose b, -c choose d) with a,b,c,d
natural numbers and then defining equivalence relations between the
first and second slots. Putting this sort of thing into Isabelle seems
reasonable but I don't know how (yet) and hopefully I don't have to
since gchoose exists.
Ray
Email Gateway (Aug 22 2022 at 15:08):From: Lawrence Paulson <lp15@cam.ac.uk>
There are quite a few ways of constructing new types in Isabelle, including inductive or coinductive constructions and quotients. But you shouldn’t need to do that to prove these binomial identities. Several of the earlier ones on your list have been proved already in Isabelle.
Larry Paulson
Email Gateway (Aug 22 2022 at 15:08):From: Raymond Rogers <raymond.rogers72@gmail.com>
Thanks! I have worked my way through the beginning facts. Mostly on
auto-pilot but I have to start somewhere; I'm kinda slow. Starting on
Formal_Power_Series (fps) theory. That looks a little harder but is
great; since it has examples in the .thy file. Actually the fps is quite
impressive and probably has all of the obvious Gould requirements.
As another exercise: do you know if anybody has encoded Roman's "Umbral
Calculus" reasoning? If not, I might do it. He does an excellent job
explaining and
I have a variation that would be interesting to tie down.
Ray
Email Gateway (Aug 22 2022 at 15:09):From: Chaitanya Mangla <cm772@cam.ac.uk>
Hi Raymond,
If you're looking for reference material for lemmas in Binomial.thy, then
you can look at Concrete Mathematics by Graham, Knuth, and Patashnik. Some
of the lemmas in the theory were taken from the chapter on Binomial
coefficients (implemented using gchoose). Comments in some lemmas even
reference pages from the book.
Regards,
Chaitanya
Email Gateway (Aug 22 2022 at 15:09):From: Manuel Eberl <eberlm@in.tum.de>
I'm pretty sure we don't have anything on Umbral Calculus. We might have
a few stray identities that fall in that category by accident, but I'm
reasonably sure nobody I know of ever attempted to formalise Umbral
Calculus systematically.
Note that we have the falling factorial ("pochhammer") and Bernoulli
numbers and Bernoulli polynomials ("bernoulli" and "bernpoly" in the AFP
entry "Bernoulli"), I think are relevant for umbral calculus.
Cheers,
Manuel
Last updated: Apr 25 2024 at 04:18 UTC