Repository navigation
Do on the one-sided path what the two-sided one does - #697
Happypig375 merged 3 commits into
Conversation
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #697 +/- ##
==========================================
- Coverage 80.99% 80.44% -0.55%
==========================================
Files 155 156 +1
Lines 13687 12929 -758
Branches 1957 2125 +168
==========================================
- Hits 11086 10401 -685
+ Misses 1990 1922 -68
+ Partials 611 606 -5 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
The one-sided path skipped everything the two-sided path has, in front of
the descent and behind it.
In front, four transformations ran only under `side is BothSides`: the
sec/csc rewrite, the substitution of finite sub-limits, and the first and
second remarkable limits. Without the second one, (1 + x)^(1/x) at 0+ is
read by the descent as 1^(+oo), and it answers 1 -- definitely, not as a
NaN -- where the same expression approached from both sides gives e. Each
of the four is guarded on a two-sided limit, and a two-sided limit that
exists is also the limit from either side, so hoisting them above the
dispatch says nothing one-sided they did not already say two-sided.
Behind, there was nothing at all:
if (side is ApproachFrom.Left or ApproachFrom.Right)
return expr.ComputeLimitDivideEtImpera(x, dest, side);
The descent can make an indeterminate form definite on the way down, by
putting a part's own limit in place of the part. x * ln(x) at 0+ becomes
0 * ln(x), so 0 * -oo, so NaN -- and NaN is the claim that the limit does
not exist, not that it was not found. sin(x) / x from either side came
back the same way: the library said the most familiar limit in the subject
did not exist. Where nothing above answers, this now moves x out to
infinity and asks there, which is what ComputeLimitImpl does for a finite
destination in any case. Whatever the descent found is kept if that finds
nothing better, so it can only add answers.
The substituted expression is simplified before being asked about, and not
for tidiness: the destination is left behind as a term, and it is exactly
that leftover which produces the NaN. (0 + 1/x) * ln(0 + 1/x) at infinity
is NaN where (1/x) * ln(1/x) is 0.
Measured over 30 one-sided limits worked out by hand: 14 correct and 15
wrong before, 22 correct and 7 wrong after. Nothing that was right became
wrong. Suite unchanged at 3m06s.
Seven remain wrong and this does not claim them. Three want the machinery
at infinity to be stronger and answer once the differences-at-infinity and
Gruntz branches are in, with no further change here. The others --
(1 - cos(x))/x^2, 1/x - 1/sin(x) and csc(x)*x -- do not, and csc(x)*x
shows why: the rewrite turns it into (1/sin(x))*x, a product, and the
first remarkable limit only matches a quotient.
Part of #209.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
7ea4508 to
0175d73
Compare
Rafael-SOWNet
changed the title
|
CI, run on my fork across the full matrix, since the run here is held at https://github.com/Rafael-SOWNet/AngouriMath/actions/runs/30926523989
The branch it ran on, |
The rule was reached from the two-sided path only, so a one-sided limit of a quotient the descent has no reading of had nothing behind it at all. It is the same rule either way: l'Hopital's is stated one-sidedly to begin with, and the two-sided case is the two one-sided ones agreeing. The side is carried through rather than dropped, because both questions the rule asks along the way can have a one-sided answer and no two-sided one. The first step of (1 - cos(x)) / x^3 reaches sin(x) / (3x^2), which is +oo on the right and -oo on the left; asked about both sides at once it comes back NaN and the step is wasted. Measured on a corpus of 49 one-sided limits with known answers: 36 correct without carrying the side and calling the rule at all, 40 with the rule but asked two-sided, 42 with the side carried. No answer changed for the worse in any of the three. csc(x) * x is the one worth naming: the csc rewrite leaves the product (1 / sin(x)) * x, which the descent does not take apart, and the rule reads it back as the quotient x / sin(x). One-sided corpus 36/49 -> 42/49. Two-sided corpus unchanged at 101/117, 0 wrong. Suite 4041 passed, 0 failed.
|
Follow-up commit The rule was reached from the two-sided path only, so a one-sided limit of a quotient the descent has no reading of had nothing behind it at all. It is the same rule either way — l'Hopital's is stated one-sidedly to begin with, and the two-sided case is the two one-sided ones agreeing. Carrying the side rather than dropping it is load-bearing, and I measured that rather than assuming it. Both questions the rule asks along the way can have a one-sided answer and no two-sided one: the first step of On a corpus of 49 one-sided limits with known answers:
No answer changed for the worse at any step. Two-sided corpus unchanged at 101/117 with 0 wrong / 0 error / 0 timeout, measured with and without the change on this same branch. CI on the fork, matrix run 30933608421 — success on windows-latest, ubuntu-latest and macos-latest, |
3 participants
The defect
The one-sided path skipped everything the two-sided path has — both in front of the descent and behind it.
In front, four transformations ran only under
side is BothSides: thesec/cscrewrite, the substitution of finite sub-limits, and the first and second remarkable limits. Without the second one, the descent reads(1 + x)^(1/x)at0+as1^(+oo)and answers 1 — definitely, not as aNaN:Behind, there was nothing at all:
The descent can make an indeterminate form definite on the way down, by putting a part's own limit in place of the part.
x * ln(x)at0+becomes0 * ln(x), so0 * -oo, soNaN— andNaNhere is not "not found", it is the claim that the limit does not exist. The clearest case is not exotic:The two-sided form gives
1. Only the one-sided ones said it did not exist.The fix
Hoist the four transformations above the side dispatch. Each is guarded on a two-sided limit, and a two-sided limit that exists is also the limit from either side, so this says nothing one-sided that they did not already say two-sided. The
BothSidesblock is unchanged in behaviour — same passes, same order.Give the one-sided path the fallback. Where nothing above answers, move
xout to infinity and ask there — which is whatComputeLimitImplalready does for a finite destination, so it is the same question asked where l'Hôpital's rule and the rest of the machinery live. Whatever the descent found is kept if this finds nothing better, so it can only add answers.The substituted expression is simplified first, and not for tidiness. The destination is left behind as a term, and it is exactly that leftover which produces the
NaN:Measured
30 one-sided limits, answers worked out by hand:
masterFixed:
sin(x)/xandx/sin(x)and(1+x)^(1/x)from both sides,tan(x)/x,x*ln(x),(1+2x)^(1/x). Nothing that was right became wrong. Full suiteFailed: 0, Passed: 4035, Skipped: 14, Total: 4049, at 3m06s — unchanged, because the fallback is only consulted where the answer was already nothing or NaN.What this does not fix
Seven remain wrong, and I am not claiming them.
Three want the machinery at infinity to be stronger, not a different bridge to it —
x^2*ln(x),sqrt(x)*ln(x),x^x. Their substituted forms are0·∞at infinity, whichmastercannot do either. They answer correctly the moment #682 and #694 are in, with no further change here — on my combined branch this same corpus scores 27 of 30.The others are their own defects.
csc(x)*xshows the shape of it: the rewrite turns it into(1/sin(x))*x, a product, andApplyFirstRemarkableonly matches aDivf.(1 - cos(x))/x^2and1/x - 1/sin(x)likewise need something this PR does not add.This is part of #209 rather than the whole of it:
1/x + ln(x)at0+is still unevaluated onmaster, because the∞−∞it becomes needs #682. With that in, it gives+oo.Tests
Sources/Tests/UnitTests/Calculus/OneSidedLimitTest.cs, 26 cases. 10 fail without the source change (verified by restoringSolvers.Definition.csfromorigin/masterin place and re-running). The rest pin the one-sided answers that were already right, and that an infinite destination is left alone — the fallback must not fire where substituting forxwould mean nothing.🤖 Generated with Claude Code