Squeeze a bounded factor against a vanishing one (#723)

[Rafael-SOWNet]

Closes #723.

What was wrong

Every rule in the limits pipeline reads a limit as a value: the descent substitutes each part's own limit, l'Hopital's rule wants a determinate quotient, Gruntz compares rates of growth. sin(x) has no limit at infinity, so each of them correctly declines and the product is left indeterminate in the shape (no limit) * 0. That is why the squeeze theorem's most standard example came back unevaluated:

lim x->+oo  sin(x) / x      =>  limit(sin(x) / x, x, +oo)

The rule

The theorem does not need the factor's limit. It needs the factor to be bounded, which is a weaker fact and one that can be read off the shape: a sine, a cosine and a sign never exceed 1; an arctangent and an arccotangent stay within an interval of angles; sums, products and moduli of bounded things are bounded. That predicate, plus one case for a product and one for a quotient, is the whole of it.

It is deliberately not "has a finite limit". That is the case the rest of the machinery already covers, and asking for it here would repeat work while missing the factors this exists for — the ones with no limit at all.

Both rules live in LimitSolvers and are reached from SimplifyAndComputeLimitToInfinity, which every destination and side is normalised into, so one statement covers x -> +oo, x -> -oo and either side of a finite point.

Boundedness is a fact about a real argument

This library reads a free variable as complex, and sin(i * t) is i * sinh(t), which grows without bound. So the argument is established real before anything is claimed, which leaves

lim x->+oo  sin(a * x) / x  =>  limit(sin(x * a) / x, x, +oo)

unanswered — correctly, since it is not 0 for every a. That limit is the example in Limit's own documentation, and it prints exactly as it did.

The other half

A sine or cosine whose argument grows without bound takes every value in its range infinitely often and settles on none, so its limit does not exist. NaN says that; leaving the node unevaluated says only that no rule found one. It is asked after the theorem and not before — asked first it would settle sin(x) / x as (no limit) / (+oo).

Two tests changed rather than broke

LimitAtInfinityTest.AFormThatCannotBeSettledTerminatesWithoutClaimingAnAnswer and GruntzTest.AnOscillationIsDeclinedRatherThanGuessedAt both pinned a bare sin(x) at infinity as unevaluated, and the first says in its own summary that the answer must not become NaN "since NaN asserts that the limit does not exist rather than that it was not found."

That principle is right, and it is why the case moved rather than the assertion being loosened. Nothing in either test established non-existence, so claiming it there would have been a guess; a sine's range does establish it. The other forms in both tests — (x + sin(x)) / x, x * sin(x), x * cos(x) — are still unevaluated and stay where they are. Gruntz still declines all three; a different rule now answers one of them.

Measured

	before	after
lim x->+oo sin(x) / x	unevaluated	0
lim x->0 x * sin(1 / x)	unevaluated	0
lim x->+oo sin(x) * e^(-x)	unevaluated	0
lim x->+oo sin(x)	unevaluated	NaN
lim x->0 sin(1 / x)	unevaluated	NaN
lim x->+oo sin(a * x) / x	unevaluated	unevaluated
lim x->0 sin(x) / x	1	1
lim x->+oo (1 + 1/x)^x	e	e

29 regression cases in a new BoundedTimesVanishingTest, covering the theorem in both shapes, the answers that were already given by the descent, the complex-argument guard and the arguments that settle rather than oscillate.

Unit tests 4807 -> 4834 passing with none failing; F# 130 of 130; the 117-problem solver corpus stays at 112 solved with 0 wrong, 0 error and 0 timeout; suite 3m33s -> 3m28s.

🤖 Generated with Claude Code