Repository navigation
Take no undecided limit for an infinite one in l'Hôpital's rule - #2360
Merged
Merged
Conversation
Whether a limit diverges was read off whether an infinity occurs in it, and an unevaluated limit(sin(u), x, +oo) holds one, as its destination. So l'Hopital's rule took sin(u) / cos(u), with neither part's limit taken, for oo/oo and differentiated it: tan(x^2 + x - 1) from the left at 0 answered -cos(-1) / sin(-1), 0.642, where the limit is tan(-1), -1.557. The same on 2.6.0. The rule, and the two places that build its quotients, now ask DivergesDecidedly, which turns an undecided limit away. The rewrites that ask IsInfiniteNode only whether they are worth trying keep it: f^g as e^(g ln f) is an equality whatever f does. Two answers had been reached through the mistake. The Stirling limits read -x + ln(2 pi x)/2 at +oo, asked from the left, unevaluated, as infinite -- which it is. An infinity has only one side and the one-sided path lacks the machinery the two-sided one has there, so a side asked for at a real infinity is now the two-sided limit; that also answers x - sqrt(x^2 + x) at +oo, -1/2, and e^x x at -oo, 0, both unevaluated before. And log(x, tanh(x))^(x^(pi + x)) at 0+ was 1 only because its base came back undecided; decided, it tends to 1 and the exponent to 0. A power whose base tends to a number other than 0 and whose exponent tends to 0 now answers 1. limitcheck, DEPTH=3, seeds 14, 16, 19, 23, 26 against master 37f7377: the limit is another value 11 -> 6, each of the five now unevaluated, and one limit more answered. Found at SEED=26; no issue was filed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## master #2360 +/- ##
==========================================
- Coverage 86.78% 86.77% -0.01%
==========================================
Files 312 312
Lines 68809 68815 +6
Branches 20045 20048 +3
==========================================
+ Hits 59713 59714 +1
- Misses 4911 4918 +7
+ Partials 4185 4183 -2
Flags with carried forward coverage won't be shown. Click here to find out more.
🚀 New features to boost your workflow:
|
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
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.
tan(x^2 + x - 1)from the left at 0 answered-cos(-1) / sin(-1), which is 0.642. The limit istan(-1), which is -1.557. 2.6.0 gives the same wrong answer.Whether a limit diverges was read off whether an infinity occurs in it. An unevaluated
limit(sin(u), x, +oo)contains one, as its destination. So l'Hôpital's rule tooksin(u) / cos(u), with neither part's limit taken, for oo/oo and differentiated it. The rule, and the two places that build its quotients, now askDivergesDecidedly, which turns an undecided limit away. The rewrites that askIsInfiniteNodeonly to decide whether to try are unchanged, because they are equalities wherever they apply.Two answers had been reached through the same mistake, and are now reached properly:
-x + ln(2 pi x)/2at+oofrom the left, unevaluated, as infinite, which it happens to be. This also answersx - sqrt(x^2 + x)at+oo(-1/2) ande^x xat-oo(0).log(x, tanh(x))^(x^(pi + x))at 0+ had been answered only while its base came back undecided.limitcheck, DEPTH=3, seeds 14, 16, 19, 23 and 26, against master 37f7377:
The five wrong values removed are all now unevaluated, and one limit more is answered (seed 23). One of those five was a right answer on 2.6.0:
log(x^x, 3/2) - 1from the left at -1 is-1 - 0.129 i, and earlier 2.7.0 changes had already turned it into-1. It is recorded in BREAKING-CHANGES.md with the rest. Suite, AOT and the harnesses are green locally.Found by limitcheck at
SEED=26; no issue was filed.🤖 Generated with Claude Code