Read a factorial's logarithm outside the power form too (#765)

[Rafael-SOWNet]

Closes #765. Follows #764, which is merged.

What was wrong

Stirling's expansion arrived inside SolveAsIndeterminatePower — the rule that turns f^g into e^(g * ln f) — so it found a factorial only under a vanishing exponent. ((x!)/x^x)^(1/x) was answered and ln(x!)/x was not, which is the harder question answered and the easier one left. ln(n!) ~ n*ln(n) is the standard statement of the result.

lim x->+oo ln(x!) / (x * ln(x))     was  unevaluated   is  1
lim x->+oo ln(x!) / x               was  unevaluated   is  +oo
lim x->+oo ln(x!) / x^2             was  unevaluated   is  0
lim x->+oo ln(x!) - x * ln(x)       was  unevaluated   is  -oo
lim x->+oo ln((2*x)!) / (x*ln(x))   was  unevaluated   is  2
lim x->+oo ln(x!) / ln(x)           was  NaN           is  +oo

The last was a wrong answer rather than a missing one — NaN claims the limit does not exist, and that quotient is asymptotic to x, reaching 9.6e11 at x = 1e12.

The guard is the work

Applying the expansion wherever a factorial's logarithm appears is not sound. What Stirling drops is 1/(12f), and an expression can be built around exactly that term:

x * (ln(x!) - (x*ln(x) - x + ln(2*pi*x)/2))   is  1/12,  and an unguarded rewrite answers 0

#764 could state its guard as power / f -> 0 because it knew the shape it was in: the answer there is e^(power * ln(base)), so power is the coefficient the dropped term gets multiplied by. Anywhere else that coefficient has to be found — by putting a variable where the logarithm is and differentiating with respect to it. The rewrite is refused unless coefficient / f vanishes.

The coefficient is put back in terms of the logarithm before it is judged, since an expression need not be linear in it: for ln(x!)^2 the derivative is 2*ln(x!), which grows like 2*x*ln(x) and is refused — correctly, since the difference of the squares is ln(x)/6 and diverges.

The guard is sufficient rather than necessary, and a test records the gap: x*ln(x!) - x^2*ln(x) is -oo, which the dropped 1/12 would not have changed, and it is refused anyway because nothing available here tells it apart from the case that is exactly 1/12.

Placement

In SolveByRewriting, the position reached only once it is settled that the expression as written has no answer. That is where it belongs: the rewrite asks for sub-limits of its own (the factorial's argument must diverge, and the coefficient must be judged), so it must not sit in the descent that visits every part of every expression.

What it costs

lim x->+oo ln((x+1)!) / (x*ln(x)) was unevaluated in about a second and now takes longer than 20 s to be unevaluated. The rewrite is right and the expression it hands over is right — the machinery cannot take that limit quickly, which is demonstrable without any of this:

lim x->+oo ((x+1)*ln(x+1) - (x+1) + ln(2*pi*(x+1))/2) / (x*ln(x))    times out on master

So the cost is the machinery's rather than this rewrite's. Recorded in BREAKING-CHANGES.md.

Measured

70 generated factorial expressions — x!, (2*x)!, (x+1)!, x!/x^x, x!/e^x, x^x/x!, (x+1)!/x! under ten wrappers — diffed against master:

	count
unevaluated → a value	13
NaN → +oo	3
unevaluated → timeout	1

24 of the 70 already timed out before this change. Every value checked numerically with mpmath at 40 digits up to x = 1e12 — ln(x!)/(x*ln(x)) approaches 1 from below and slowly, reaching only 0.9638 there, so the corpus value is easy to get wrong by eye.

• casbench 113/117, 0 wrong, 0 error, 0 timeout — unchanged
• unit tests 5322 passed, 0 failed (5307 on master; 15 added)
• F# wrapper tests 130 passed
• propcheck 0 failures, rootcheck 596/596, simpsweep 0 disagreements of 10463