Answer the limits that come out as infinity minus infinity

[Rafael-SOWNet]

Builds on #680 — the first commit here is a fix to that branch, and the diff will shrink to the second commit once #680 lands.

What was wrong

lim x -> +oo of e^x - x, of x - ln(x) and of sqrt(x^2 + x) - x all came back unevaluated. Every solver reads either a polynomial or a substitution of +oo into the expression, and a difference of two parts that each grow without bound is neither — substituting gives oo - oo, which says nothing.

What it does now

One part outgrows the other. Then the answer is that part's, which is what the ratio of the two says: x / e^x tends to 0, so e^x - x tends to +oo.

The two grow alike. The ratio tends to 1 and says nothing, and then a - b = (a² - b²) / (a + b) — an identity wherever a + b is not zero, which on the way to +oo it is not. It is worth using where squaring removes a root: the leading terms of the numerator cancel and an ordinary quotient is left.

lim x->+oo sqrt(x^2 + x) - x   →  x / (sqrt(x^2 + x) + x)  →  1/2

Neither reading works on a root of a polynomial, because no solver can say anything about one. sqrt(x^2 + x) is now written x * sqrt(1 + 1/x), which puts its growth in plain sight and leaves a factor +oo can simply be substituted into. That is sound in the one direction it is used: P = x^d * (P / x^d), and (uv)^r = u^r v^r wants u positive, which x^d is on the way to +oo; a destination of -oo has already been turned into +oo by substituting -x for x.

Falling out of that: sqrt(x^2 + x) / x, x / sqrt(x^2 + 1), sqrt(4x^2 + 1) / x and sqrt(x^2 - x) / x now have answers too.

Simplification is asked again, since it can hand back an expression of another kind altogether and which parts a limit is broken into is decided by that kind. sqrt(x^2 + 1) / sqrt(x^2 + 3x) is broken up as a quotient, while what simplifying gives is the single root sqrt((x^2 + 1) / (x^2 + 3x)), whose argument can be read straight off. 2.2 s to reach no answer before, 14 ms to reach 1 now.

Cost

All of it is reached only once the expression as written has been found to have no answer, so nothing that already had one is asked twice. It sits beside l'Hopital's rule rather than in the descent that visits every part of every expression — putting it there instead cost the test suite four times its running time, which is how the placement was chosen.

The first commit

While measuring this I found that the rule added in #680 could run for over twenty seconds on lim x -> +oo sqrt(x^2 - x) / x, which master answers, unevaluated, in 190 ms. A bound on the depth is not a bound on the work: each step asks what the two parts of its quotient tend to before differentiating them, and each of those is a limit the rule may be applied to in turn, so the steps fan out rather than follow one another. The rule now declines a quotient it is already partway through, and one that has grown by more than the derivative of a power or a logarithm accounts for. Both forms are pinned as terminating.

Not covered

sqrt(x^2 + 3x) - sqrt(x^2 + 1), where the parts grow alike and the conjugate is a quotient the solvers cannot read either — left unevaluated, and pinned as terminating. An odd degree under the root: the growth of sqrt(x^3 + x) is x^(3/2), and a quotient containing that is one the rule above is stopped from working on. Genuine oo - oo where the difference is decided by more than the leading terms (e^(x + e^(-x)) - e^x) needs Gruntz's algorithm and is a separate piece of work.

Verification

3937 unit tests and 127 F# tests on both target frameworks, none failing. A 117-problem self-verifying corpus goes from 91 to 93 with nothing wrong, in error or timing out, and the oo - oo family is complete. 1320 property checks over 151 expressions, none failing.

18 of the 27 new tests fail without the source change; the 9 that pass are the ones pinning what already worked.

[codecov-commenter]

⚠️ Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

❌ Patch coverage is 85.36585% with 12 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.51%. Comparing base (90c00a8) to head (5fa2b66).
⚠️ Report is 56 commits behind head on master.

Files with missing lines	Patch %	Lines
...ath/Functions/Continuous/Limits/Transformations.cs	85.00%	5 Missing and 7 partials ⚠️
❗ Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

@@            Coverage Diff             @@
##           master     #682      +/-   ##
==========================================
- Coverage   80.99%   80.51%   -0.48%     
==========================================
  Files         155      156       +1     
  Lines       13687    12977     -710     
  Branches     1957     2145     +188     
==========================================
- Hits        11086    10449     -637     
+ Misses       1990     1920      -70     
+ Partials      611      608       -3     

☔ 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]

Rebased onto master now that #680 has landed. The first of the two commits was part of #680 and is already in, so this is down to the one commit. 4022 tests, none failing.