A power of the variable times a sine or cosine of a logarithm, and a power of a monomial - #1479
Merged
Merged
Conversation
…power of a monomial `x^2 sin(a + b ln(c x^n))` and `(c x^n)^b` were both left as written. The first is a closed form, not a search: two rounds of parts close on the integrand, the sine's remainder being the cosine's integral and the cosine's the sine's, so the pair is solved rather than iterated. `int x^m sin(L) dx` is `x^(m+1)((m+1) sin(L) - B cos(L))/((m+1)^2 + B^2)` wherever `L' = B/x`, which `a + b ln(c x^n)` is with `B = b n`. Differentiating the answer is the whole proof. The hyperbolic twin needs no rule -- `sinh` is written as exponentials, which fold against the logarithm -- while the sine and cosine are nodes that fold against nothing. The second distributes `(c x^n)^b` into `c^b x^(n b)`, for a positive `c` and a `n` that is not whole. Both conditions are the domain's: with a fractional or symbolic `n` the integrand is real only where `x > 0`, and there the identity holds; with a whole `n` it is real at a negative `x` too, and there `(c x^n)^b` is a power of `|x|` -- `(2 u^3)^(3/2)` is `2^(3/2) sgn(u) u^(9/2)`, and distributing it without the sign is a wrong answer, which the rules for a root of an even power already avoid. Both conditions come from a measured failure rather than from care: the first version of this had no `n` condition and the suite's `ARootOfAnEvenPowerIsNotThePower` caught the lost sign at depth, under `u = tan(x)`; and the closed form's divisor `(m+1)^2 + B^2` is `9 + (n sqrt(-9/n^2))^2` for one row of Rubi's 4.7.5, a zero that only `Simplify` folds -- an imaginary `B` of that size makes the two rounds circular rather than closing, and the answer divided by nothing at all. The corpus reported it as a wrong answer; it is declined now. Family 4 of the Rubi suite: 289 -> 290 of 422, 0 wrong, 0 error; family 1 158/228 and the 1774-problem suite 1707 unchanged. Suite 12671 passed; allocation gate passed on all 19 gated benchmarks. Part of #718. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
x^2 sin(a + b ln(c x^n))and(c x^n)^bwere both left as written. Two rules, and both of their side conditions were written by a measurement rather than by foresight.The trigonometric of a logarithm is a closed form. Two rounds of parts close on the integrand — the sine's remainder is the cosine's integral, the cosine's is the sine's — so the pair is solved rather than iterated:
int x^m sin(L) dxisx^(m+1)((m+1) sin(L) - B cos(L))/((m+1)^2 + B^2)whereverL' = B/x, whicha + b ln(c x^n)is withB = b n. Differentiating the answer is the whole proof. The hyperbolic twin needs no rule at all — the library writessinhas exponentials, which fold against the logarithm (#1470) — whilesinandcosare nodes that fold against nothing.A power of a monomial is distributed,
(c x^n)^b→c^b x^(n b), for a positivecand a non-wholen. Both conditions are the domain's: with a fractional or symbolicnthe integrand is real only wherex > 0, and there the identity is exact; with a wholenit is real at a negativextoo, and there the value is a power of|x|.What the measurement caught, in the order it caught it:
n, and family 4 leapt +13 — all of it unsound. At depth, underu = tan(x), the rule saw(2 u^3)^(3/2)and distributed it to2^(3/2) u^(9/2), dropping thesgn(u)that the root-of-an-even-power rules write. The suite's ownARootOfAnEvenPowerIsNotThePowerfailed on exactly that integrand. With the condition, the gain is +1 and the sign is back.x^2 sin(a + ln(c x^n) sqrt(-9/n^2)), where the closed form's divisor(m+1)^2 + B^2is9 + (n sqrt(-9/n^2))^2— a zero that onlySimplifyfolds. An imaginaryBof exactly that size makes the two rounds circular rather than closing, so the "closed form" divided by nothing at all. It is declined now, and the divisor is tested symbolically.Measured (final build):
familycap.sh 4 6): 289 → 290/422, 0 wrong, 0 error — 4.7.5 goes 2 → 3 of its 6.bench.sh: PASSED on all 19 gated benchmarks.x^m cos(a + b ln(c x^n))) — worst relative deviation 0.Part of #718.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura