Limits: a power whose exponent moves is compared against the wrong thing, and lim x->+oo x^x / e^(x*ln(x)) gives 0 where it is 1 #735

x ^ x and e ^ (x * ln(x)) are the same function, so this expression is identically 1:

"x ^ x / e ^ (x * ln(x))".ToEntity().Limit("x", "+oo")   // 0

It comes back 0. The library's own evaluator disagrees with its own limit -- (50 ^ 50) / e ^ (50 * ln(50)) evaluates to exactly 1.

It is not one expression. Every quotient of a moving-exponent power against an exponential of the matching logarithm answers 0, whatever the true value:

x ^ x / e ^ x and x ^ x / 2 ^ x are right (+oo), so this is not "powers with a moving exponent are broken" -- it needs the two sides to be in the same comparability class, which is exactly when Gruntz's algorithm is the rule that answers.

Cause

Gruntz.Mrv reads a power b ^ p with x in the exponent as exp(p * ln(b)) and puts that constructed node in the mrv set, but nothing rewrites the expression itself. Gruntz.Rewrite then substitutes members by name, with Substitute(member, ...), so a member that does not occur in the expression as written is never found.

With GRUNTZ_DEBUG=1 the set comes back holding the same exponential twice:

mrv(x ^ x / e ^ (ln(x) * x)) = {e ^ (x * ln(x)), e ^ (ln(x) * x)}
rewrite -> = x ^ x / (e ^ 0 * (1 / %1) ^ 1)   logw=-ln(x) * x
leadterm(x ^ x / e ^ (ln(x) * x)) = (x ^ x, 1/1)

Once as the constructed e ^ (x * ln(x)) and once as the denominator's own e ^ (ln(x) * x) -- the same product with its factors the other way round, since simplification sorted the one that was already in the expression and the constructed one was never sorted. Only the second is found. x ^ x survives into the series, its leading exponent reads as +1, and w ^ positive tends to zero, so the algorithm concludes 0.