Repository navigation
The cosecant, the secant, and a linear denominator in the cosine, by the half-angle substitution - #1238
Conversation
…the half-angle substitution int 1/sin(x) and int 1/cos(x) had no antiderivative. They are table entries in every calculus text, and the gap was easy to miss because the neighbours are answered: tan(x) comes out, and so does 1/sin(x)^2 through the cotangent rule. Measured against Rubi's suite with the harness able to finish a run for the first time, the band it rates as a *single table lookup* is the worst-served difficulty we have -- 58%, barely above the 52% for problems needing two or three rules -- and this family is a large part of why. Under t = tan(x/2), sin(x) = 2t/(1+t^2), cos(x) = (1-t^2)/(1+t^2) and dx = 2/(1+t^2) dt, so an integrand built from sines and cosines by the field operations becomes a quotient of polynomials, which partial fractions already answers -- and answers 50x faster since #1236. 1/sin(x) -> ln(tan(x/2)) 1/(1+cos(x)) -> tan(x/2) 1/cos(x) -> a logarithm of a quotient linear in tan(x/2) Two judgement calls worth stating. Simplify rather than InnerSimplified on the rewritten integrand, because the rewrite puts a quotient inside a quotient and partial fractions wants one Divf of two polynomials. InnerSimplified leaves the nesting, so every one of these was handed on in a shape nothing downstream could read. And the Providedf that collapsing the nesting attaches is dropped. It says 1 + t^2 != 0, which is not vacuous over the complex plane -- it fails at t = +-i, and complex is this library's default codomain. It is sound to drop because of what t is here: t = tan(x/2) reached by rewriting a real trigonometric integrand, so the excluded points are not reachable values of it and do not appear in the answer, which is written back in terms of x. The answer is an antiderivative on each interval between the poles of tan(x/2) rather than across one. That is the standing property of this substitution and the same one SolveByTangentSubstitution already carries. What this does not reach, and why, is a simplifier gap rather than a gap here: Simplify never puts a sum over a common denominator, so 1/(1-sin(x)) rewrites to 2/((t^2+1)*(1 + (-2)t/(t^2+1))) and stays there. Even `a + b/c` is left split. That is the operation other systems call together or ratsimp, and it is what the rest of this family needs. Filed separately. Every answer is checked by differentiating it back and comparing at five points, never against a printed form. Full suite green: 8499 and 1485. #718 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
CI caught this and my local run did not, because I ran Sources/Tests/UnitTests
and not the F# wrapper's suite, which pins the readable answer.
cos(x) + 1 is a function of the cosine alone, so the rewrite succeeds on it and
produces a correct antiderivative in tan(x/2) about forty characters long:
expected sin(x) + x + C
actual 4 * (2 * tan(x/2) / (tan(x/2)^2 + 1) + 2 * 2 * arctan(...) / 2) / 4 + C
Both are antiderivatives and only one is an answer anybody wants. Everything
that decomposes the problem into pieces the ordinary rules know now gets first
refusal, and this sees only what is left -- which is still the quotients it was
added for, since linearity declines a quotient and partial fractions declines
one that is not a ratio of polynomials. 1/sin(x), 1/cos(x) and 1/(1 + cos(x))
are unchanged.
Three cases pinning the decline, so this does not come back.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
|
Pushed a fix for the red check, which was a real defect rather than flake.
Both are antiderivatives; only one is an answer anybody wants, and that test pins the readable one. The rule was sitting before It now runs after linearity. Everything that decomposes the problem into pieces the ordinary rules know gets first refusal, and this sees only what is left — still the quotients it was added for, since linearity declines a quotient and partial fractions declines one that is not a ratio of polynomials.
Suites run this time rather than assumed: UnitTests 8,499 and 1,493, FSharpWrapperUnitTests 134, InteractiveWrapperUnitTests 18, TerminalUnitTests 41. |
Part of #718.
int 1/sin(x)andint 1/cos(x)had no antiderivative. They are table entries in every calculus text, and the gap was easy to miss because the neighbours are answered:tan(x)comes out, and so does1/sin(x)^2through the cotangent rule.Why this family, measured rather than chosen
With
intbenchable to finish a run for the first time, the band Rubi rates as a single table lookup is the worst-served difficulty we have:A one-step lookup should be our best band, not a point above our second. Reading the 112 that fail, they cluster on rational functions of sine and cosine.
What it does
Under
t = tan(x/2):sin(x) = 2t/(1+t^2),cos(x) = (1-t^2)/(1+t^2),dx = 2/(1+t^2) dt. So an integrand built from sines and cosines by the field operations becomes a quotient of polynomials — which partial fractions already answers, and answers 50x faster since #1236.Two judgement calls, stated rather than buried
Simplifyrather thanInnerSimplifiedon the rewritten integrand. The rewrite puts a quotient inside a quotient, and partial fractions wants oneDivfof two polynomials;InnerSimplifiedleaves the nesting, so every one of these was handed on in a shape nothing downstream could read.The
Providedfis dropped, and it is worth being exact rather than calling it vacuous. It says1 + t^2 != 0, which fails att = ±i— and complex is this library's default codomain. It is sound to drop because of whattis here:t = tan(x/2), reached by rewriting a real trigonometric integrand, so the excluded points are not reachable values of it and do not appear in the answer, which is written back in terms ofx.The answer is an antiderivative on each interval between the poles of
tan(x/2)rather than across one. That is the standing property of this substitution and the same oneSolveByTangentSubstitutionalready carries.What it does not reach, and why that is not this rule's fault
1/(1-sin(x)),1/(1+cos(x)/2),1/(2cos(x)+3sin(x))still decline. They rewrite correctly and then stop, becauseSimplifynever puts a sum over a common denominator — evena + b/cis left split. That is the operation other systems calltogetherorratsimp, we do not have it, and it is what the rest of this family needs. Filing it separately.Checked
Every answer differentiated back and compared at five points inside one branch, never against a printed form. Two cases assert the rule correctly declines:
sin(x) + xis not a function of the sine alone, andsin(x)*sin(2x)leaves anxbehind becausesin(2x)is notsin(x)— the right outcome, since a product of sines wants product-to-sum. Full suite green: 8,499 and 1,485.🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura