Compute limits at infinity by Gruntz's algorithm (#231, #353)

[Rafael-SOWNet]

Implements what #353 proposes and links the paper for, which #231 also asks for.

"e^(x + e^(-x)) - e^x".Limit("x", "+oo")        // master: unevaluated → 1
"sqrt(x^2+3*x) - sqrt(x^2+1)".Limit("x","+oo")  // master: unevaluated → 3/2
"x^20/e^x".Limit("x", "+oo")                    // master: unevaluated → 0
"x/sqrt(x^2+1)".Limit("x", "+oo")               // master: unevaluated → 1

The first is the standard demonstration. Expanding the two exponentials separately gives two divergent series whose difference cancels entirely — so no amount of differentiating both halves arrives anywhere. Rewriting the whole expression in w = e^(-x) gives (e^w - 1)/w, whose leading term is 1.

Two pieces

AsymptoticSeries — a power series in w about 0 with real exponents and symbolic coefficients. It could not be a Taylor series: the coefficients are expressions in x and the exponents may be negative and fractional. It takes the value of log(w) from outside, since w is an exponential whose logarithm is an ordinary expression — without it the constant term of log(c·w^e) cannot be told from zero. How far to carry it is not known in advance, so the caller raises the order until a leading term survives the cancellation.

Gruntz — finds the subexpressions in the fastest comparability class, writes each as a power of one of their number, and reads the answer off the leading term.

Three things the thesis is emphatic about, all of which cause silent wrong answers if missed, are honoured and commented as such:

• exp(s - c·t) is never split into a product of exponentials, which would put back a function of a faster class. (This is the bug that makes SymPy 1.14 answer limit((x!/x^x)^(1/x), x, oo) with 0 instead of 1/e — I verified that against a local install.)
• The member everything is rewritten in terms of is one with no other member inside it.
• The leading coefficient is checked to be free of w before its exponent is trusted.

Scope, and what it declines

The exp-log functions — what is built from x and the rationals with the four operations, exp and log — which is what the algorithm is stated for, because those are eventually monotone and so comparable at all. A sine has no limit at infinity and no comparability class either, so this declines rather than guesses, and that is pinned. So is the factorial, which needs Stirling and a tractable-function mechanism this does not have.

Only for a destination at infinity. A limit at a finite point reaches infinity too, by substituting for x, but there this would be replacing answers the existing rules already give rather than adding ones they do not. Concretely: lim x → 0 x^x comes out as 1, against an existing test (TestNoLimit) that pins it as having no limit. Over ℂ, 1 is defensible; over ℝ the two-sided limit does not exist. That is a change to argue on its own evidence, not to make as a side effect of this, so it is out of scope here.

Verification

21 new tests: six that nothing before could reach, twelve ordinary competing growths that must come out unchanged, and three oscillations pinned as declined-and-terminating.

4028 unit tests and 127 F# tests on both target frameworks, none failing. 117-problem self-verifying corpus with nothing wrong, in error or timing out; 1320 property checks over 151 expressions, none failing.

GRUNTZ_DEBUG=1 prints the recursion tree — the algorithm calls itself by four different routes and any failure surfaces as a plain decline, so there is no following it otherwise.

[codecov-commenter]

Codecov Report

❌ Patch coverage is 78.35821% with 87 lines in your changes missing coverage. Please review.
✅ Project coverage is 81.54%. Comparing base (90c00a8) to head (6fc4949).
⚠️ Report is 74 commits behind head on master.

Files with missing lines	Patch %	Lines
...iMath/Functions/Continuous/Limits/Gruntz/Gruntz.cs	71.35%	24 Missing and 31 partials ⚠️
...tions/Continuous/Limits/Gruntz/AsymptoticSeries.cs	84.95%	12 Missing and 19 partials ⚠️
...ns/Continuous/Limits/Solvers/Solvers.Definition.cs	75.00%	0 Missing and 1 partial ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master     #694      +/-   ##
==========================================
+ Coverage   80.99%   81.54%   +0.54%     
==========================================
  Files         155      159       +4     
  Lines       13687    13749      +62     
  Branches     1957     2318     +361     
==========================================
+ Hits        11086    11211     +125     
+ Misses       1990     1883     -107     
- Partials      611      655      +44     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[Rafael-SOWNet]

Two notes after integrating this with the other open branches.

It answers a form #682 pins as unanswerable. That PR adds AFormNeitherReadingSettlesTerminatesWithoutClaimingAnAnswer, asserting that sqrt(x^2 + 3x) - sqrt(x^2 + 1) comes back as an unevaluated Limitf. That is true of the conjugate reading on its own — the two parts grow alike, so the ratio says nothing and the conjugate is a quotient the solvers cannot read. The series settles it at 3/2, and sqrt(x^2 + 3x) - sqrt(x^2 + 5x) at -1.

Neither branch answers those alone; only the two together do. Whichever of the two lands second should turn that test from a non-answer into the answer, and I will push that as part of this PR if #682 goes in first. Flagging it rather than leaving it to surface as a red build.

Two small things fixed on this branch since it was opened (force-pushed, no review had happened yet):

• an orphaned comment left in Solvers.Definition.cs after the call it described moved
• x ^ 20 / e ^ x was silently dropped from the "cannot settle" theory rather than moved. It is now an InlineData on CompetingGrowthAtInfinity asserting 0, with a note that nothing about l'Hopital's step bound changed — the answer comes from one leading term instead of twenty derivatives.