mathlib vs the literature

Stream: mathlib4

[Johan Commelin]

I want to discuss the following PR by @Scott Carnahan, because it has been sitting in limbo for a while, and I think it brings up an interesting question. Here's the PR in question:

chore: shift Nat.ascFactorial down by one #7965

The tl;dr summary is:

1. docs#Nat.ascFactorial is currently misaligned with conventional maths literature
2. The diff makes me think that mathlib got the definition right, and the literature got it wrong

On the one hand, we want mathlib to stay close to established conventions, at the same time we don't want to make our lives more difficult.

Here's a random thought I had, about what we might do:
We keep both definitions (as stdName and stdName', where the primed version departs from literature conventions). We then prove how the two notions relate, and keep on working with stdName' mostly.
Landmark results could be stated in two versions, with a short proof of the conventional statement that simply rewrites it in terms of the other statement and applies the other version.

Happy to hear other peoples thought on this matter.

[Eric Wieser]

Can you elaborate a little more on which bits of the diff particularly support 2)?

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/pull/7965/files#diff-07d04a046d145326d6b194de8cc9f54deb9c9b0aee2e2f458919db2685eec351R235-R252

[Geoffrey Irving]

Does this mean we can have the off-by-one-fixed version of the gamma function?

[Johan Commelin]

Lol, I guess $\Gamma'$ will be understood as the derivative :oops: :see_no_evil:

[Ruben Van de Velde]

Why are those new statements using natural subtraction? :)

[Yaël Dillies]

I was the one defining nat.asc_factorial. I definitely followed (some subset of) the literature.

[Eric Rodriguez]

It's got an interesting history, as I defined it originally to prove something about cardinality of injective functions, and then yael noticed I had the names the wrong way round and swapped them to what we had to day. Maybe their lean3 pr is indicative of this?

[Reid Barton]

Do you have a reference? I looked at all arXiv results for "rising factorial" and in every one that defined some notation like $(x)^{\overline n}$, it was defined in the normal way (starting from $x$). Wikipedia also does not suggest that there is any other convention in use.

[Reid Barton]

I think Johan will be able to predict that I am strongly in favor of using the convention that is in use, as far as I can tell, everywhere other than mathlib.

[Reid Barton]

Or using the fulltext search, just scroll through
https://search.arxiv.org/?in=&query=%22ascending%20factorial%22

[Scott Carnahan]

I would be very interested to see suggestions for statements that do not use natural subtraction (or are otherwise easier/more natural)!

[Kevin Buzzard]

The definition can be written as the product of $n+i$ for $i\in$ List.range k, and there's no natural subtraction there. Neither the definition in the PR nor the original definition uses natural subtraction either.

[Scott Carnahan]

Sorry for the ambiguity. The statement in question from #7965 that uses natural subtraction (and has a rather messy proof) is:

theorem ascFactorial_eq_factorial_mul_choose (n : ℕ) : ∀ (k : ℕ),
    n.ascFactorial k = k ! * (n + k - 1).choose k

[Kevin Buzzard]

Oh I see. Yeah that is a bit weird. I'm happy with Johan's idea of making the apparently-more-useful-but-not-in-the-literature function just a primed version and keeping it.

[Scott Carnahan]

With the primed definition, we would have Nat.ascFactorial' n k = Nat.ascFactorial (n+1) k. Should we instead consider the following course:

1. no primed definition
2. any results that use natural subtraction (e.g., n+k-1) also have primed versions with n+1 as input parameter. For example,

theorem ascFactorial_eq_factorial_mul_choose' (n : ℕ) : ∀ (k : ℕ),
    (n + 1).ascFactorial k = k ! * (n + k).choose k

[Kevin Buzzard]

Then you need another theorem covering the zero case (which is fine)

[Scott Carnahan]

I would like to suggest a third alternative: replace Nat.ascFactorial with some new Ring.ascFactorial for any semiring, since the definition immediately generalizes to that setting. I made such a definition in #6934, but maybe I should put it in a separate file with fewer dependencies. Is there an advantage to keeping a special version for natural numbers around?

[Kyle Miller]

I think it's worth keeping Nat.ascFactorial around as a definition with few dependencies, having a Ring.ascFactorial n k = Nat.ascFactorial n k lemma (not simp), and in the Nat.ascFactorial documentation mentioning Ring.ascFactorial.

[Alex J. Best]

Why do you think that Kyle? I can't think of too many things that you could do with nat factorial without the semiring structure on Nat, which seems like all you'd need for the general def.

[Yaël Dillies]

@Scott Carnahan, this already exists: docs#ascPochhammer.

[Yaël Dillies]

I see from your PR that you know about it. Then I'm dubious of its necessity.

[Scott Carnahan]

I see - please disregard the third alternative.