ascending/descending factorial notation

Stream: general

[Yaël Dillies]

We're trying to come up with nice notation for the ascending ((n + k)!/n!) and descending (n!/(n - k)!) factorials. I'm pretty partial to nꜝk for the ascending one, but there isn't an index version. Here's what searching for "exclamation" on the Unicode website yields:

• n!k
• n¡k
• nǃk
• n‼k I swear this symbol is great for double factorial
• n⁈k
• n⁉k
• n❕k
• n❗k
• n❢k
• n❣k
• nꜝk This one could be nice for the ascending factorial
• nꜞk Maybe this one for the descending factorial?
• nꜟk Or this one?
• n︕k
• n﹗k
• n！k
  Which do you prefer? Also, do you like the layout n <operator> k?

[Alex J. Best]

Its not pretty but you could also try and approximate the Pochammer symbol notation withn⁽k⁾ (untested if this can work in lean)

[Yaël Dillies]

I was thinking about n^(k) and n_(k) but it doesn't look that great and it always bugged me that ascending adn descending factorials weren't using exclamation marks.

[Alex J. Best]

I do like the symmetry of pairs like n¡k nǃk and nꜝk nꜞk. Did you look at https://en.wikipedia.org/wiki/Falling_and_rising_factorials#Alternate_notations the superscript + and minus versions there could work? Or of course just P(n,k)...

[Mario Carneiro]

I will be very sad if there are big computations involving nꜝk / nꜞk. At reasonable distances they are not distinguishable

[Mario Carneiro]

honestly I think n^(k) and n_(k) are better, although there are probably other issues with that

[Mario Carneiro]

how about n !+ k and n !- k

[Yaël Dillies]

I'm now defining the notation: infix !⁺ :50 := asc_factorial.
What's the correct priority?

[Mario Carneiro]

probably somewhere around +, *, ^ : what do you want to be higher priority?

[Yaël Dillies]

I think we want !⁺ to have priority.

[Mario Carneiro]

so a ^ b !+ c means a ^ (b !+ c)?

[Yaël Dillies]

Or rather I think it fits between + and ^

[Mario Carneiro]

* is also between those

[Yaël Dillies]

It should probably be below *

[Yaël Dillies]

I think we more often want to multiply an ascending factorial than to ascend factor(?) a product.

[Kevin Buzzard]

You can use #print notation * to see the priority of everything. There is no right answer here. You have to decide what you want a * b !+ c to mean.

[Mario Carneiro]

so between 65 and 70 then. Should it be equal to either one?

[Kevin Buzzard]

You could see how other notations are used in the literature.

[Mario Carneiro]

a lot of other things have prec 65 or 70 since that means they get ordered in the same left associative class

[Mario Carneiro]

like + and - are both 65

[Mario Carneiro]

so that a + b - c means (a + b) - c and a - b + c means (a - b) + c

[Yaël Dillies]

Ah sorry, I meant that !⁺ should have priority over *

[Kevin Buzzard]

When we were defining things like external direct sums and products $\bigoplus_i A_i$ etc we looked in the literature to see how these things were used. We had to decide what mathematicians meant by $\prod_i a_i + c$

[Kevin Buzzard]

If people are using notation like ${}_nP_k$ or whatever then it should have a very high priority.

[Mario Carneiro]

#print notation is even better since it shows all notations (although it would be nice to sort it by priority)

[Yaël Dillies]

Yeah, exactly.

[Mario Carneiro]

scalar smul has priority 73

[Yaël Dillies]

But I don't think we ever use a ^ b !⁺ c as a ^ (b !⁺ c)

[Yaël Dillies]

However a !⁺b ^ c could be (a !⁺b) ^ c

[Mario Carneiro]

oh, you want them to be equal prec?

[Yaël Dillies]

Parsing it as a !⁺ (b ^ c) is fine, though

[Mario Carneiro]

also, FWIW I still think it's better without unicode

[Mario Carneiro]

it's literally "+ k"

[Yaël Dillies]

Yeah but isn't like conflicting notation with +?

[Mario Carneiro]

no, !+ is a token

[Mario Carneiro]

or will be

[Yaël Dillies]

Okay then :)

[Mario Carneiro]

it will cause a problem if someone wants to write a!+b to mean a! + b but we put spaces in that kind of thing anyway by style guide

[Yaël Dillies]

So infix !+ :74 := asc_factorial is fine?

[Eric Wieser]

(a zulip tip - use double backticks for code containing ` , triple backticks for code containing `` , etc)

[Mario Carneiro]

you should put spaces around it like infix ` !+ `:74 := asc_factorial, which makes it appear with spaces around it when pretty printed

[Yaël Dillies]

I already have :smile:

[Scott Morrison]

How about just no notation? I think unfamiliar notation is generally worse than nothing.

[Yaël Dillies]

Have you had a look at the PR? (#7759) It looks nice in my opinion.

[Eric Wieser]

I think it would be best not to introduce new notation in the same PR as one that swaps around definition names - it would be much easier to review whether the notation is a good idea if it were a PR that did nothing other than switch existing lemmas to the new notation

[Yaël Dillies]

Okay sure. Will split