Double factorials

Stream: Is there code for X?

[Jake Levinson]

I'm going to introduce a PR for double factorials shortly, intended for use in a later PR on an explicit formula for the coefficient of a Hermite polynomial. Any suggestions on API? Here's the working definition:

@[simp] def double_factorial : ℕ → ℕ
| 0       := 1
| 1       := 1
| (k + 2) := (k + 2) * double_factorial k

notation n `‼`:10000 := double_factorial n -- this is \!! not two !'s

So far I only plan to have

lemma double_factorial_def (n : ℕ) : (n + 2) ‼ = (n + 2) * n ‼ := rfl
lemma double_factorial_def' (n : ℕ) : (n + 1) ‼ = (n + 1) * (n - 1) ‼ := by { cases n; refl }

[Adam Topaz]

maybe $n!! * (n+1)!! = (n+1)!$ is another useful lemma? Where do these show up besides Hermite polynomials? Is the genrealization from parity to congruence modulo $m$ for general $m$ useful at all?

[Jake Levinson]

Hmm, I think of double factorials as showing up in combinatorics. For example there are $(2n+1)!!$ leaf-labeled trivalent trees on $n+3$ labels. (Also the moduli space of genus 0 stable curves.)

[Jake Levinson]

They also come up in Catalan combinatorics, which means they get involved in various objects that involve associativity.

[Jake Levinson]

Hmm, another useful lemma would be $(2n)!! = 2^n n!$.

I don't think I've encountered the variant with congruence mod $m$.

[Adam Topaz]

I see. Maybe some of our resident combinatorialists (I'm certainly not one of them ;)) have some ideas as well?

[Kyle Miller]

We should probably have double_factorial n = prod i in range ((n + 1) / 2), (n - 2*i), or whatever the correct statement is

[Jake Levinson]

Ugh, nat.sub

[Jake Levinson]

How about a subtraction-free version (dependent on whether n is even or odd)?

[Kyle Miller]

I'd be happy with a $(2n)!!$ and a $(2n+1)!!$ formula (that way it also avoids nat division)

[Yaël Dillies]

Can we skip double factorials and directly go to m-factorials? 1-factorials are factorials, 2-factorials are double factorials, etc... Most of the lemmas you can write about double factorials directly generalise to those.

[Adam Topaz]

That's what I meant about congruence mod m above. Where do these m factorials show up (just curious)?

[Kyle Miller]

For general $m$, I think mostly you see $m^nn!$ for the "$m$-factorial" of $mn$, and they quickly show up when you do things with the generalized binomial theorem. I'm not sure I've really encountered the other $m-1$ of them.

[Kyle Miller]

though a priori they're a way to partition a factorial into $m$ products, which seems like it must have been useful to someone at some point

[Eric Wieser]

I don't think replacing nat.factorial with nat.factorial' 1 is worth the churn (especially mid-port), but I can see the appeal of skipping 2-factorials and having just the 1- special case and the general n- version.

[Jake Levinson]

I asked a combinatorialist colleague and she had never encountered the $m$-variation. One thing that's special about $m=2$ is that the formula @Adam Topaz gave, combined with the formula I gave, means that both $(2n)!!$ and $(2n+1)!!$ show up individually in various formulas where you can divide out a power of 2. In contrast for $m > 2$ I don't know where the other terms would show up individually.

[Eric Wieser]

Don't all the formulae up-thread hold with the 2s replaced with $m$?

[Kyle Miller]

No, $n!_m \cdot (n+1)!_m = (n+1)!$ doesn't hold (I replaced 2 with $m$), though $n!_m\cdot(n+1)!_m\cdots (n+m-1)!_m=(n+m-1)!$ does (I made up the notation here).

When $m=2$ the reason $(n+1)!!$ seems to be interesting is that it's the complement of $n!!$ in $(n+1)!$, like Jake said.

[Kyle Miller]

Besides it seeming like there's no math about it yet, one reason against defining nat.factorial' is the question of what nat.factorial' 0 should be...

[Adam Topaz]

$n!_0$ is the empty product, right? So it should be 1?

[Adam Topaz]

Isn’t there some generalized gamma function behind the scenes? That should give us a hint about what this should be.

[Kyle Miller]

Isn't the formula $n!_m = n(n-m)(n-2m)\cdots$ where the product continues until you get to something less than $m$? There are roughly $n/m$ terms, so $n!_0$ is the infinite product $n(n-0)(n-2\cdot 0)(n-3\cdot 0)\cdots$

[Adam Topaz]

Maybe it’s just n? I was thinking of the fact that Z/0 is Z, so when you take the product of all ints between 1 and n which are congruent mod 0 to n, you get just n. (The gamma function has a shift in the relationship with the factorial, so maybe it does end up being an empty product from that point of view, I don’t know.)

[Kyle Miller]

We could look at $(mn)!_m = m^nn!$, so reparameterizing that's $(a)!_b=b^{a/b}(a/b)!$ and you can use a gamma function there to extend it. I wonder if the $b\to 0$ limit converges here?

[Kyle Miller]

Oh, that can't be the right formula... According to this, $(5)!_2 = 15\sqrt{\pi/2}$ rather than $15$ :smile:

Anyway, if it were correct then we'd get $(0)!_0=1$, $(1)!_0=0$, $(2)!_0=0$, and then $(a)!_0=\infty$ for $a\geq 3$.

[Jake Levinson]

#18994

[Jake Levinson]

This has the lemmas suggested by @Adam Topaz and @Kyle Miller, but not multifactorials.

[Jake Levinson]

For what it's worth, many of these other generalizations can be formulated as ∏ i in finset.range n, whatever, if they are ever needed. For now, my intended use case is the odd double factorial (which seems to be the one I've encountered most often).

[Kevin Buzzard]

Yeah from the point of view of the gamma function I think the even and odd double factorials are two different functions which interpolate in two different ways