From 1785c0ee7be0d63e5a3b6cabd80f7f897b8fbbbd Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 13 Nov 2026 13:02:50 +0000 Subject: [PATCH] Leave a two-sided limit undecided where a side stops at a finite form beside real values A two-sided limit asks each side outright when the descent's sides come back NaN. A side that stops at an indeterminate form with an infinity in it counts as undecided (#2419); one of finite parts, 0 / 0 or c / 0, counted as a side without a limit, which made the two-sided limit NaN. That is right for (x - x) / (x - x), which has no value anywhere, and wrong for erf(abs(x)) / x^4 at 0, which is +oo from each side: the form there is two parts whose rates were never compared. Such a side now counts as undecided where the expression has a finite real value at 10^-6 and 10^-9 from the point on that side. Where it has none -- (x - x) / (x - x), or ln(-2) / ln(x) at 1, complex beside the point -- the side still has no limit and the two-sided limit stays NaN. Co-Authored-By: Claude Opus 5.5 --- BREAKING-CHANGES.md | 13 +++++++ .../Limits/Solvers/Solvers.Definition.cs | 34 +++++++++++++++---- ...ecidedSideLeavesTheLimitUnevaluatedTest.cs | 12 ++++++- 3 files changed, 51 insertions(+), 8 deletions(-) diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index f12988228..a70ca6bd5 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -101,6 +101,19 @@ and 1 in order. 2.6.0 answered the third with a wrong `0`. Found by limitcheck; | `"x^2 * floor(1/x^2)".ToEntity().Limit("x", 0)` | `0` | `limit(x ^ 2 * floor(1 / x ^ 2), x, 0)` | | `"x * ceil(1/x)".ToEntity().Limit("x", 0)` | `NaN` | `limit(x * ceil(1 / x), x, 0)` | +### A two-sided limit whose side stops at a finite indeterminate form is left unevaluated + +**Silent: a two-sided limit is left unevaluated, rather than answered, where a side's limit stops at an indeterminate +form of finite parts, such as `c / 0`, and the expression is real just beside the point.** That form is a side whose +parts were never compared, not a side without a limit. `1 / log(x^2, cos(x))` is `+oo` from each side of 0, and 2.6.0 +answered `-oo`; `1 / (x * arccot(x))` is `+oo` from each side, and 2.6.0 answered `NaN`. Where the expression has no real value beside the point, as `(x - x) / (x - x)` has none anywhere, the +limit is still `NaN`. Found by limitcheck; no issue was filed. + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"1 / log(x^2, cos(x))".ToEntity().Limit("x", 0)` | `-oo` | `limit(1 / log(x ^ 2, cos(x)), x, 0)` | +| `"1 / (x * arccot(x))".ToEntity().Limit("x", 0)` | `NaN` | `limit(1 / (x * arccotan(x)), x, 0)` | + ### A limit at the jump of a step function is not answered by substitution **Silent: a limit of an expression built on `floor`, `ceil`, `round` or `sgn`, where the step's argument arrives on one diff --git a/Sources/AngouriMath/Functions/Continuous/Limits/Solvers/Solvers.Definition.cs b/Sources/AngouriMath/Functions/Continuous/Limits/Solvers/Solvers.Definition.cs index 259d70522..f3a9c027e 100644 --- a/Sources/AngouriMath/Functions/Continuous/Limits/Solvers/Solvers.Definition.cs +++ b/Sources/AngouriMath/Functions/Continuous/Limits/Solvers/Solvers.Definition.cs @@ -193,12 +193,12 @@ node is Floorf or Ceilf or Roundf or Signumf bothSidesDepth++; try { - var fromLeft = Decided(ComputeLimit(expr, x, dest, ApproachFrom.Left)); + var fromLeft = Decided(ComputeLimit(expr, x, dest, ApproachFrom.Left), ApproachFrom.Left); if (fromLeft?.Evaled == MathS.NaN) return null; // A side that does not exist settles the question whatever the other side does, // so the right is still asked when the left is undecided. - var fromRight = Decided(ComputeLimit(expr, x, dest, ApproachFrom.Right)); + var fromRight = Decided(ComputeLimit(expr, x, dest, ApproachFrom.Right), ApproachFrom.Right); if (fromRight?.Evaled == MathS.NaN) return null; if (fromLeft is null || fromRight is null) @@ -215,15 +215,35 @@ node is Floorf or Ceilf or Roundf or Signumf // where it stops the search, and withheld at the outermost call, where it is not an // answer. One with an infinity in it, 0 * floor(-oo) for x floor(2/x), is a product or // a quotient of parts whose rates were never compared, so that side is undecided rather - // than absent. One of finite parts only stays a side without a limit, as before: 0 / 0 - // for (x - x) / (x - x), which has no value anywhere, and ln(-2) / 0 for ln(-2) / ln(x) - // at 1, whose sides are infinities in different directions. - static Entity? Decided(Entity? limit) + // than absent. So is one of finite parts where the expression takes real values on that + // side: erf(abs(x)) / x^4 at 0 stops at 0 / 0 from each side, is +oo from each, and was + // NaN. One of finite parts stays a side without a limit where the expression has no real + // value beside the point: 0 / 0 for (x - x) / (x - x), which has no value anywhere, and + // ln(-2) / 0 for ln(-2) / ln(x) at 1, whose values there are not real and whose sides + // are infinities in different directions. + Entity? Decided(Entity? limit, ApproachFrom side) => limit is { } && IsAnIndeterminateForm(limit) - && limit.Nodes.Any(static node => node is Real { IsFinite: false }) + && (limit.Nodes.Any(static node => node is Real { IsFinite: false }) + || IsRealBeside(expr, x, dest, side)) ? null : limit; } + /// + /// Whether has a finite real value at two points on + /// of a finite real , 10^-6 and 10^-9 away. + /// A witness that the expression is defined and real there, not a proof of it near + /// every point; a side it finds real is only ever left undecided, never answered. + /// + private static bool IsRealBeside(Entity expr, Variable x, Entity dest, ApproachFrom side) + { + if (dest.Evaled is not Real { IsFinite: true } at || side is ApproachFrom.BothSides) + return false; + var sign = side is ApproachFrom.Left ? -1 : 1; + return RealAt(Rational.Create(sign, 1_000_000)) && RealAt(Rational.Create(sign, 1_000_000_000)); + bool RealAt(Rational offset) + => expr.Substitute(x, at + offset).Evaled is Real { IsFinite: true }; + } + /// /// Whether is real on both sides of a real , /// close enough to it, but for its constants, decided structurally: every power to an exponent that is not whole, diff --git a/Sources/Tests/UnitTests/Calculus/AnUndecidedSideLeavesTheLimitUnevaluatedTest.cs b/Sources/Tests/UnitTests/Calculus/AnUndecidedSideLeavesTheLimitUnevaluatedTest.cs index b81941078..728948028 100644 --- a/Sources/Tests/UnitTests/Calculus/AnUndecidedSideLeavesTheLimitUnevaluatedTest.cs +++ b/Sources/Tests/UnitTests/Calculus/AnUndecidedSideLeavesTheLimitUnevaluatedTest.cs @@ -13,7 +13,8 @@ namespace AngouriMath.Tests.Calculus /// /// A two-sided limit whose sides stopped at an indeterminate form with an infinity in it, 0 * floor(-oo) for /// x floor(2/x) at 0, answered NaN, which says there is no limit, where each side is 2. Such a side is undecided, - /// so the limit is left unevaluated. Found by limitcheck; no issue was filed. + /// so the limit is left unevaluated. So is a side that stops at a form of finite parts, 0 / 0 for erf(abs(x)) / x^4, + /// where the expression is real beside the point. Found by limitcheck; no issue was filed. /// [Trait("Area", "Calculus")] public sealed class AnUndecidedSideLeavesTheLimitUnevaluatedTest @@ -23,6 +24,14 @@ public sealed class AnUndecidedSideLeavesTheLimitUnevaluatedTest [InlineData("floor(1/x) * sin(x)")] [InlineData("x^2 * floor(1/x^2)")] [InlineData("x * ceil(1/x)")] + // A side that stops at 0 / 0, or at c / 0, of an expression real beside the point is undecided too: + // erf(abs(x)) / x^4 is +oo from each side, 1 / log(x^2, cos(x)) is +oo, abs(x)^erf(x) is 1. + [InlineData("erf(abs(x)) / x^4")] + [InlineData("erf(abs(x)) / (x^3 * sinh(x))")] + [InlineData("1 / log(x^2, cos(x))")] + [InlineData("abs(x)^erf(x)")] + [InlineData("tan(1/2 + x) + abs(x)^erf(x)")] + [InlineData("1 / (x * arccot(x))")] public void IsNotNaN(string input) => Assert.IsType(input.ToEntity().Limit("x", 0)); @@ -30,6 +39,7 @@ public void IsNotNaN(string input) // in different directions, an oscillation, a jump. [Theory] [InlineData("(x - x) * sin(x) / ((x - x) * x)", "0")] + [InlineData("(x - x) / (x - x)", "0")] [InlineData("ln(-2) / ln(x)", "1")] [InlineData("sin(1/x)", "0")] [InlineData("floor(2/x)", "0")]