Choose on integer

Stream: Is there code for X?

[Bin Wu]

I want to find a def of "choose" on integer. When I useNat.choose n k, sometimes I need n or k be negative. I know the definition on math, but haven't find a def on integer in mathlib.
In this case, If a < b , a - b = 0 in natural number. This is not what I wanted.

[Kim Morrison]

How do you want to extend it?

[Bin Wu]

follow this definition:

$$\binom{n}{k} =\left\{\begin{matrix} \frac{n^{\underline{k} }}{k!}, & k \ge 0 \\ 0, & k < 0 \end{matrix}\right.$$

where n,k : integer, underline{k} means descPochhammer.

[Jz Pan]

Do you want docs#Ring.choose over Z?

[Bin Wu]

Ring.choose r n still need natural number n

[Andrew Yang]

What does $n^{\underline{-1}}$ mean? Is it $\frac{1}{n+1}$?

[Bin Wu]

When k < 0, we just use the second line.

[Andrew Yang]

Ah I missed it.
How is that useful for k < 0? Is there any result that hold over all k?

[Bin Wu]

Here is an example

$$\sum\limits_{k=0}^{m} \binom{m}{k} \binom{n}{r-k}k=\binom{m+n}{r} \dfrac{rm}{m+n}$$

I think it should holds even if r < (m + n)

[Jz Pan]

Bin Wu said:

Ring.choose r n still need natural number n

Do you think it's good to extend the definition of Ring.choose to, say, Ring.ichoose, which allows n to be Int? Let's ask the author of Ring.choose.

[Johan Commelin]

cc @Scott Carnahan

[Scott Carnahan]

If we think of Ring.choose r n as the x ^ n coefficient of a formal expansion of (1 + x)^r in R[[x]], then this expanded definition amounts to saying the expansion has no negative-exponent terms in R((x)). It looks pretty harmless as a generalization, and I would be interested to see what identities extend. Are there references in the literature?

[Mauricio Collares]

That's the definition of binomial coefficients in Concrete Mathematics, for example

[Mauricio Collares]

In fact, Knuth makes a point of using this convention as much as possible to simplify manipulations, as explained in this excerpt from The Art of Computer Programming

[Mauricio Collares]

KnuthBinomial.png

[Scott Carnahan]

Thank you for the reference! Ring.ichoose sounds like a good idea. Is there a way to avoid complete duplication of identities?

[Sébastien Gouëzel]

I read in the above text that Knuth is a big fan of well-chosen junk values, just like Mathlib :-)

[Bin Wu]

Can lean handle this?
$n : \mathbb{Z}$, if $n \ge 0$, then we can restrict n to a natural number ($n : \mathbb{N}$).

[Jz Pan]

Bin Wu said:

Can lean handle this?
$n : \mathbb{Z}$, if $n \ge 0$, then we can restrict n to a natural number ($n : \mathbb{N}$).

You can see the definition of $\mathbb{Z}$ in Lean: docs#Int :

inductive Int : Type where
  | ofNat   : Nat → Int
  | negSucc : Nat → Int

so maybe you can write:

match n with
| ofNat n => Ring.choose r n -- in this case n is non-negative
| _ => 0 -- in this case n is negative

[Ruben Van de Velde]

As it happens, this definition exists as docs#Int.toNat

[Bin Wu]

Then I think Ring.ichoose is achievable!

[Yaël Dillies]

Bin Wu said:

Can lean handle this?
$n : \mathbb{Z}$, if $n \ge 0$, then we can restrict n to a natural number ($n : \mathbb{N}$).

If you have n : ℤ and hn : 0 ≤ n, then the tactic lift n to ℕ using hn will give you n : ℕ

[Julian Berman]

With no illusion that we'll be successful as I don't know the math, (we're learning as we go), last week at the NYC meetup, and probably this afternoon, we were working on generalizing factorials to arbitrary dedekind domains.

[Julian Berman]

I see elsewhere in the papers I was flipping through that once that's done there's a general binomial coefficient defined on top of them, though I'm not sure yet if it's the same one as Ring.choose.

[Kevin Buzzard]

What is the factorial of $i$ in $\mathbb{Z}[i]$? What is the factorial of $-1\in\Z$? I'm curious about how this works.

[Yaël Dillies]

Is this any different to docs#descPochhammer ?

[Julian Berman]

https://www.sciencedirect.com/science/article/pii/S0022314X9892220X is one of (the 3) papers

[Julian Berman]

Yaël Dillies said:

Is this any different to docs#descPochhammer ?

yes it's different from that

[Kevin Buzzard]

And also different to docs#Nat.descFactorial ?

[Julian Berman]

(Kevin I don't know how to calculate it yet honestly for specific values.)

[Jz Pan]

Kevin Buzzard said:

What is the factorial of $i$ in $\mathbb{Z}[i]$? What is the factorial of $-1\in\Z$? I'm curious about how this works.

Gamma function :rolling_on_the_floor_laughing:

[Scott Carnahan]

As far as I can tell from the paper, Bhargava defines generalized factorials as ideals, not elements.

[Kevin Buzzard]

yeah it looks like a totally different thing. For example the prime 3 is inert in $D=\mathbb{Z}[i]$ and the idea is that the 3-adic valuation of this generalized factorial will be 0 up to nu_9(D,(3)) where it's forced to go up to 1 because you've run out of elements of the residue field.

[Julian Berman]

Ok, if it's totally unrelated then ignore me clearly!