Integration by parts descends on the total power of its transcendental factors, takes two of them against a polynomial whose antiderivative is chosen to match, and a logarithm or an arctangent of a polynomial is closed at any depth

[Rafael-SOWNet]

Charlwood's x arctan(x)^2 ln(1 + x^2) is thirteen of Rubi's steps and
had no antiderivative here; so had arctan(x) ln(1 + x^2), and
x ln(1 + x^2) arctan(x), and ln(1 + x^2) anywhere but at the top. Four
things, each a rule about the same step.

The measure by parts descends on read the highest power of a logarithm or
inverse trigonometric factor; it reads the total now, per term of a sum
and the largest of those. arctan(x) ln(1 + x^2) is two, and one step of
parts leaves 2x^2 arctan(x)/(1 + x^2) - x ln(1 + x^2)/(1 + x^2), each term
of which is one -- the step differentiated one of the two away, and that
is the descent it made, where the highest power read one on both sides
and declined the larger remainder. A step that lowers the total may grow
the expression, and a step that keeps it must shrink the expression, as
before, so the pair is well-founded as before.

Two such factors are taken together against the rest of the integrand
whose integral is algebraic; against nothing, whose integral is x, they
were not, for want of a rest. They are now. And the antiderivative of the
rest is fixed up to a constant, and the constant is chosen so that what
the pair's derivative divides by divides it: against
arctan(x)^2 ln(1 + x^2) the antiderivative of x is (1 + x^2)/2 and not
x^2/2, and the remainder is arctan(x) ln(1 + x^2) + x arctan(x)^2, two
products each answered by parts, where with x^2/2 it was two quotients
by 1 + x^2 that are elementary only together. Rubi's x^m rules do the
same. Where the two together are not elementary -- x ln(1 + x^2) arctan(x)
taken together leaves ln(1 + x^2)/(1 + x^2), which is not -- one of them
is differentiated and the other integrated beside the rest, either way
round: by parts against x ln(1 + x^2), whose integral is a substitution,
with the arctangent differentiated, the remainder is
(ln(x^2 + 1) (x^2 + 1) - x^2)/(2 (x^2 + 1)). Which the expanding split
took apart into x^2 ln(x^2 + 1)/(2 (x^2 + 1)) and ln(x^2 + 1)/(2 (x^2 + 1)),
neither elementary; a sum over a denominator is split as written first
now, each term over it with a factor written on both sides cancelled, and
as written it is ln(x^2 + 1)/2 - x^2/(2 (x^2 + 1)).

By parts against one is a rule of the top: a nested step's remainder
answered that way let a doomed search above it carry on. So ln(1 + x^2)
one level down had no antiderivative, and every remainder that held it
was declined for want of it. The logarithm, arctangent or arccotangent of
a polynomial is the same step for the one shape whose remainder is
closed -- x f(P) - int x f'(P) P', the remainder rational, to the rational
integrator directly -- and is closed itself, so it is answered at any
depth.

Rubi sample (463 problems, 5 s budget), against the #1318 master this branch is cut from:

master at #1318     409/463, 0 wrong, 0 timeouts, ~97 s
with this           410/463, 0 wrong, 0 timeouts, 97 s

One more, nothing lost: Charlwood 143, in 0.6 s. No other problem moved by more than noise. One thing was measured on the way and is not in this branch: the pair's derivative simplified before the product respelled 1 + x^2 as x^2 + 1, and Charlwood 74 -- x arctan(x) ln(x + sqrt(1 + x^2))/sqrt(1 + x^2), the test this rule was written for -- lost its substitution to the spelling; the derivative is taken as differentiation writes it.

Independent of #1319, merged meanwhile; the two touch the split at different places.

The five test suites are green.

Part of #718.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura