Repository navigation
Apply l'Hopital's rule at infinity too (#596) - #680
Merged
Happypig375 merged 2 commits intoAug 4, 2026
Merged
Conversation
The rule was only ever reached when the destination was finite, so the ordinary competing-growth limits had nothing to catch them: lim x->+oo ln(x) / x was unevaluated, and NaN once simplified lim x->+oo x / e^x " lim x->+oo ln(x) / sqrt(x) " lim x->+oo e^x / (e^x + 1) " Three things had to be settled before the rule could be let loose there. It has to stop. Differentiating both parts does not always make the quotient simpler: x / sqrt(x^2 + 1) turns into sqrt(x^2 + 1) / x, which turns back, so neither form ever settles. The recursion is bounded, at a depth that still leaves room for the degree of a polynomial, since x^10 / e^x takes ten steps. It has to leave a wrong answer no worse. NaN asserts that a limit does not exist, which is a stronger claim than the rule can make when it has not settled, so the rule's answer is only taken when it is not NaN; otherwise whatever was there before stands, unevaluated included. It has to recognise the quotient. Two shapes were being turned away: - Differentiation does not produce quotients. d/dx ln(x)^2 is 2 * ln(x) * (1 / x), a product with a quotient inside rather than 2 * ln(x) / x, and only the second has a limit here, so the derivative quotient is simplified before it is used. The domain condition that simplification leaves behind is dropped with it: a Providedf is not a continuous node and would be turned away unread, and limits already treat the expression as continuous. - A product with a reciprocal factor is a quotient. That is the shape in #596, where lim x->+oo x^4 * e^(-x) came out as NaN while x^4 / e^x gave 0. Corpus 88/117 -> 91/117 with no wrong answers: lim:oo/oo goes to 4 out of 4 and x / ln(x)^2 joins it. 3909 unit tests and 127 F# tests pass, and the property checker's 1320 checks are clean. Still out of reach and still left unevaluated rather than guessed: e^x - x, sqrt(x^2 + x) - x and e^(x + e^(-x)) - e^x, none of which is a quotient.
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #680 +/- ##
==========================================
- Coverage 80.99% 80.19% -0.81%
==========================================
Files 155 156 +1
Lines 13687 12686 -1001
Branches 1957 2075 +118
==========================================
- Hits 11086 10173 -913
+ Misses 1990 1921 -69
+ Partials 611 592 -19 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
The rule as added in this branch could run for more than twenty seconds on lim x -> +oo sqrt(x^2 - x) / x and on x^(3/2) * sqrt(1 + 1/x^2) / x^2, both of which master answers, unevaluated, in under two hundred milliseconds. The bound on the depth was not a bound on the work. Every 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 and sixteen deep is far more than sixteen steps. Two conditions stop the fan-out at its source: the rule declines a quotient it is already partway through, since differentiating sqrt(x^2 - x) / x gives its reciprocal and differentiating that gives the first back; and it declines one that has grown by more than the derivative of a power or a logarithm accounts for, since a bigger quotient makes the two questions each step asks harder than the one being answered. The measured room is wide: a step on the way to an answer adds two nodes and the most any was seen to add is six, against eighteen for the quotient above. A cap on the total number of applications is left behind them as a backstop. Depth is now held for the whole of the rule rather than only for its recursive call, so the two limits each step asks for are counted as well. Both forms now terminate, the second of them in 86 ms, and the two are pinned. Every limit the branch already answered is unchanged and no faster or slower: x^10 / e^x still takes ten steps and 40 ms. 3911 tests, corpus 91/117 with nothing wrong, in error or timing out.
2 of 3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Addresses part of #596, and a class of limits that had no answer at all.
What was missing
l'Hopital's rule is already implemented, but
ComputeLimitonly reaches it on the branch for a finite destination. At infinity the call simply returns whateverComputeLimitDivideEtImperafound, so the textbook competing-growth limits had nothing to catch them:Three things had to be settled first
It has to stop. Differentiating both parts does not always make the quotient simpler —
x / sqrt(x^2 + 1)turns intosqrt(x^2 + 1) / x, which turns back — so the recursion is bounded. The bound leaves room for the degree of a polynomial, sincex^10 / e^xtakes ten steps.It must not make an answer worse.
NaNasserts that a limit does not exist, which is a stronger claim than the rule can make when it has not settled. Its answer is only taken when it is notNaN; otherwise whatever was there before stands, unevaluated included.It has to recognise the quotient. Two shapes were being turned away:
d/dx ln(x)^2is2 * ln(x) * (1 / x)— a product with a quotient inside, not2 * ln(x) / x— and only the second has a limit here. The derivative quotient is now simplified before use, and the domain condition that simplification leaves behind goes with it, since aProvidedfis not aContinuousNodeandComputeLimitturns it away unread. Limits already treat the expression as continuous;SimplifyAndComputeLimitToInfinitydrops the same node for the same reason.Effect
lim x->+oo ln(x) / x0lim x->+oo x / e^x0lim x->+oo ln(x) / sqrt(x)0lim x->+oo ln(x)^2 / x0lim x->+oo e^x / (e^x + 1)1lim x->+oo x / ln(x)^2+oolim x->+oo x^3 / ln(x)+oolim x->+oo ln(ln(x)) / ln(x)0lim x->+oo sqrt(x) / sqrt(x + 1)1lim x->+oo x^10 / e^x0lim x->+oo x^4 * e^(-x)0Verification
x / sqrt(x^2 + 1),(x + sin(x)) / x,x^20 / e^x) asserting that each terminates and stays unevaluated rather than hanging or claimingNaN.lim:oo/oogoes to 4 out of 4.Not covered
e^x - x,sqrt(x^2 + x) - xande^(x + e^(-x)) - e^xare still unevaluated — none of them is a quotient, and rewriting anoo - ooas one is a separate piece of work (#231, #353). They are left unevaluated rather than guessed.