diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index f2e47d4f4..57f7237a3 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -307,17 +307,66 @@ either now; and the secant quotient was simplified to `cos/(b^(5/2) d)` through `(1/cos)^(3/2) = cos^(-3/2)`, which is wrong for every negative cosine and cancelled against the same wrong step on the denominator. On the 1774-problem independent suites this is 1707 to 1705, the two `asin` rows, with the sign error gone. +### A rational function of a sine over a symbolic quadratic in it is integrated over the two roots + +**Improvement, not silent.** `sin(x)/(a + b sin(x) + c sin(x)^2)` and everything rational in +`sin(x)` and `cos(x)^2` over that quadratic came back unevaluated, or ran past any budget: +under the half-angle the quadratic in the sine is a quartic in `t` with a symbol in every +coefficient, which nothing factors, and the substitution `u = sin(x)` wants a cosine above the +bar that an even power does not give. Written in `s = sin(x)` the integrand is a rational function +of `s`, divided down and split over the written factors as any is, and the piece over the +quadratic is taken by the two roots `r = (-b ± sqrt(b^2 - 4ac))/(2c)`, each +`1/(sin(x) - r)` being `-2 atan((r tan(x/2) - 1)/sqrt(r^2 - 1))/sqrt(r^2 - 1)` for any complex +`r` — a form checked by differentiation, not a piecewise on the sign of a root, which has no +value for the conjugate pair the ordinary coefficients give. The cosine the same way, with +`-2 atan(tan(x/2)/σ)/((1 + r) σ)`, `σ = sqrt((r - 1)/(r + 1))`. On each interval between the +poles of `tan(x/2)`, as every half-angle answer. + +| | Was | Is | +|---|---|---| +| `"1/(a+b*sin(x)+c*sin(x)^2)".Integrate("x")` | unevaluated | the two arctangents over `sqrt(b^2 - 4ac)` | +| `"sin(x)^4/(a+b*sin(x)+c*sin(x)^2)".Integrate("x")` | unevaluated after more than three minutes | `(x - sin(2x)/2)/(2c) + b cos(x)/c^2 + (b^2 c - a c^2) x/c^4 + …` in 70 ms | +| `"csc(x)^2/(a+b*sin(x)+c*sin(x)^2)".Integrate("x")`, `"sec(x)^2/…"` | unevaluated | `-cot(x)/a + …`, the blocks over `sin^2` and `1 - sin^2` beside the two roots | +| `"1/(a+b*cos(x)+c*cos(x)^2)".Integrate("x")` | unevaluated | the cosine form | + +### A function comes out of a fractional power of its even power with its sign + +**Improvement, not silent.** The entry two above made `(sin(x)^2)^(3/2)` the modulus `|sin(x)|^3` +and left three of Rubi's integrands unevaluated for it, and answered two more in powers of the +modulus through the substitutions. The modulus is the function times its sign, and the sign is a +constant between the function's zeros: `(a sin(x)^2)^(5/2)` is `a^(5/2) sgn(sin(x)) sin(x)^5`, the +sign comes out in front of the integral, and what is left is a whole power any rule reads. An even +power of a real function is not negative, so `(c q)^p = c^p q^p` holds for the principal powers +whatever `c` is, and nothing is assumed about the constant — checked at `a = -3` as well as +`a = 2`. Whole products of the exponents only, at the top of the integration only, and after the +rule that does the same for a polynomial under a square root, whose answers are as they were. +[#1387](https://github.com/asc-community/AngouriMath/issues/1387) + +| | Was | Is | +|---|---|---| +| `"x*sqrt(sin(x)^2)".Integrate("x")` | unevaluated | `sgn(sin(x)) (sin(x) - x cos(x))` | +| `"(csc(x)^2)^(3/2)".Integrate("x")`, `"1/(csc(x)^2)^(7/2)".Integrate("x")` | unevaluated | `sgn(csc(x))` times the integral of `csc^3`, of `sin^7` | +| `"(sin(x)^2)^(3/2)".Integrate("x")` | `(2/3 tan(x/2)^5 + 2 tan(x/2)^3) ((2 tan(x/2))^2)^(1/2)/((tan(x/2)^2 + 1)^3)` | `sgn(sin(x)) (cos(x)^3/3 - cos(x))` | +| `"(a*sin(x)^2)^(5/2)".Integrate("x")` | `sgn(sin(x)) a^(5/2) (...)` in `(1 - abs(sin(x))^2)^(1/2)` over `sgn(cos(x))` | `sgn(sin(x)) a^(5/2) (2 cos(x)^3/3 - cos(x) - cos(x)^5/5)` | +| `"1/sqrt(a*cot(x)^2)".Integrate("x")` | `-sgn(tan(x)) ln(1/sqrt(1 + abs(tan(x))^2))/sqrt(a)` | `sgn(cot(x)) ln(1 + tan(x)^2)/(2 sqrt(a))` | +| `"(b*tan(x)^2)^(5/2)".Integrate("x")` | `sgn(tan(x)) b^(5/2) ((abs(tan(x))^2)^2/2 - abs(tan(x))^2 + ln(abs(tan(x))^2 + 1))/2` | the same with `tan(x)` for `abs(tan(x))` | + ### A condition the answer states on its own is no longer repeated beside it **Improvement, not silent.** `Simplify` returned `(1 - ln(x))/x^2 provided not x = 0` for the derivative of `ln(x)/x`, and `(1 + ln(x)) x^x provided not x = 0` for that of `x^x`. The quotient by `x^2`, the `ln(x)` and the `0^0` are each undefined at zero already, so the condition excluded a point the expression never reached and said twice what the expression says once. A `provided` -whose condition the expression proves on its own — a quotient by `d`, a negative power of `d`, a -logarithm of `d` or to the base `d`, `d^f` with `f` vanishing too, for `d` the condition's `e`, -a positive power of it, a product holding it, a polynomial in the variable `e` is with no constant -term, or a polynomial that is zero at the root of a linear `e` — comes back without that -conjunct. Only the answer is read this way, and only its top: inside a piecewise a predicate +whose condition the expression proves on its own — whose own domain condition, read in the +ambient codomain (`DomainConditionIn`), already excludes the zeros of the condition's `e`: a +conjunct `not d = 0` or `d > 0` with `d` being `e` itself, a positive power of it, a product +holding it, a sine, tangent, arcsine or arctangent of such a thing, a polynomial in the variable +`e` is with no constant term, or a polynomial that is zero at the root of a linear `e`, or a +disjunction every side of which does, as `x^x`'s `not x = 0 or x > 0` — comes back without that +conjunct. Decided by the domain condition rather than by the shape of the node, so it follows +the codomain: when [#217](https://github.com/asc-community/AngouriMath/issues/217) gives `1/0` +a value under the codomains that admit a complex infinity, the quotient's domain condition +changes there and the condition beside `1/x` stops being redundant, with no change to the rule. Only the answer is read this way, and only its top: inside a piecewise a predicate decides which case is taken and stays; inside the simplifier's own search a `provided` is what rules read as "this candidate needs a condition" and stays too. A condition the expression does not state is kept — `x/x` simplifies to `1 provided not x = 0` as before, since `1` no longer @@ -329,6 +378,7 @@ says it. [#1394](https://github.com/asc-community/AngouriMath/issues/1394) | `"x^x".Differentiate("x").Simplify()` | `(1 + ln(x)) x^x provided not x = 0` | `(1 + ln(x)) x^x` | | `"x^n".Differentiate("x").Simplify()` | `x^n n/x provided not x = 0` | `x^n n/x` | | `"1/(x^2 + x) provided not x = 0 and not x + 1 = 0".Simplify()` | unchanged | `1/(x^2 + x)` | +| `"tan(x) provided not cos(x) = 0".Simplify()`, `"sin(x)/x provided not x = 0".Simplify()` | unchanged | `tan(x)`, `sin(x)/x` | | `"(x + sin(x))/x".Limit("x", "+oo")` | unevaluated | `1`, by the squeeze theorem on `sin(x)/x` once the division no longer carries the condition between the terms | ### The Pythagorean pair is found anywhere in a sum diff --git a/Sources/AngouriMath/Docs/Contributing/SimplificationContract.md b/Sources/AngouriMath/Docs/Contributing/SimplificationContract.md index a797a3420..ce3a5d071 100644 --- a/Sources/AngouriMath/Docs/Contributing/SimplificationContract.md +++ b/Sources/AngouriMath/Docs/Contributing/SimplificationContract.md @@ -79,15 +79,22 @@ use it rather than invent a test. ### `Providedf` — a condition carried on the value -`expr provided condition` says: this equals `expr` where `condition` holds, and is undefined +`expr provided condition` says: this equals `expr` where `condition` holds, and has no value otherwise. `Simplify` already produces it — `x/x` gives `1 provided not x = 0` — and `Entity.Provided` drops the condition when it is `True`, so nothing is attached where nothing is needed. -Two costs to know before reaching for it. A condition **competes on complexity**, because `Simplify` -ranks candidates by node count, so attaching one can make a better form lose. And a condition -**travels**: it propagates outward and can escape a binder -([#878](https://github.com/asc-community/AngouriMath/issues/878)), and a single `NaN` condition inside -a `Piecewise` collapses the whole node. +**A condition the expression's own domain condition already states is redundant, and `Simplify` +drops it.** `x^x provided not x = 0` is `x^x` and `1/x provided not x = 0` is `1/x`: what an +expression accepts under a codomain is what `DomainConditionIn` says — a nonzero divisor, a +nonzero base or a positive exponent, a nonzero antilogarithm over the complex plane and a positive +one over the reals — and a `provided` that only excludes points that condition already excludes +says nothing. The decision is made against the domain condition read in the ambient codomain, not +against the shape of the node, so it follows the codomain: when +[#217](https://github.com/asc-community/AngouriMath/issues/217) gives `1/0` a value under the +codomains that admit a complex infinity, the quotient's domain condition changes there and the +`provided` beside `1/x` stops being redundant, with no change to the rule. A condition the +expression does not state stays: `x/x` becomes `1 provided not x = 0`, and `1` says nothing about +zero ([#1394](https://github.com/asc-community/AngouriMath/issues/1394)). ## 3. Four things that are not the same diff --git a/Sources/AngouriMath/Docs/Usage/Comparison.md b/Sources/AngouriMath/Docs/Usage/Comparison.md index 4e0fa6995..40ffe9549 100644 --- a/Sources/AngouriMath/Docs/Usage/Comparison.md +++ b/Sources/AngouriMath/Docs/Usage/Comparison.md @@ -110,6 +110,11 @@ library answers `x + 1 provided not x - 1 = 0`. Same for `x/x + 0*y`. Carrying a singularity costs the shorter output on those rows and is deliberate — see [SimplificationContract.md](../Contributing/SimplificationContract.md), which is where a rewrite's right to attach or drop such a condition is set out. +The two differentiation rows are the other +half of the same trade, and they no longer carry the condition: the quotient by `x^2` and the +`0^0` each exclude zero by their own domain condition, so a `provided not x = 0` beside them said +what the expression already says, and `Simplify` drops a condition its answer's domain condition +already states. The two equal-length rows differ by collection and ordering: `1 + 3 * x ^ 2 + 4 * x` against `1 + 4*x + 3*x^2` is the same polynomial written in a different order. diff --git a/Sources/AngouriMath/Functions/PredicateEntailment.cs b/Sources/AngouriMath/Functions/PredicateEntailment.cs index cc6e35fa2..313df8db8 100644 --- a/Sources/AngouriMath/Functions/PredicateEntailment.cs +++ b/Sources/AngouriMath/Functions/PredicateEntailment.cs @@ -154,26 +154,30 @@ private static bool TryRead(Entity predicate, out Entity subject, out bool above /// /// /// - /// (1 - ln(x))/x^2 provided not x = 0 is (1 - ln(x))/x^2: the quotient is - /// undefined at zero, so the condition excludes a point the expression does not reach, - /// and a reader is told twice what the expression says once. The same for - /// (1 + ln(x)) x^x provided not x = 0, where ln(0) and 0^0 are both - /// undefined. https://github.com/asc-community/AngouriMath/issues/1394 + /// (1 + ln(x)) x^x provided not x = 0 is (1 + ln(x)) x^x: 0^0 has no + /// value, so the condition excludes a point the expression does not reach, and a reader + /// is told twice what the expression says once. + /// https://github.com/asc-community/AngouriMath/issues/1394 /// /// - /// Sound whichever way "undefined" is read. A provided says the expression - /// has no value where its condition fails; dropping it changes nothing where the - /// expression already has no value there, whether that absence is written NaN or - /// a complex infinity (https://github.com/asc-community/AngouriMath/issues/217). What has - /// to be proven is that the expression is undefined at every zero of e, - /// and it is proven only structurally: a quotient by d, a negative power of - /// d, a logarithm of d or to the base d, or d^f with f - /// vanishing too, where d is e itself, a positive power of it, a product - /// holding it, or a polynomial in the variable e is with no constant term. Every - /// such node is undefined at the zeros of e, and an undefined operand makes the - /// whole expression undefined, since no operation here absorbs one. Anything not proven - /// keeps its condition: a false negative is a redundant clause, a false positive would - /// claim a value at a point. + /// Decided by the expression's own domain condition, under the codomain. A + /// provided says where the expression has a value, so a condition is redundant + /// exactly where the expression has none in the codomain the question is asked in -- + /// and what an expression accepts under a codomain is what + /// already says: a quotient accepts a nonzero + /// divisor, a power a nonzero base or a positive exponent, a logarithm a nonzero + /// antilogarithm over the complex plane and a positive one over the reals, and so on + /// through every node. The condition is redundant where that domain condition already + /// excludes the zeros of e: a conjunct not d = 0 or d > 0 with + /// d vanishing at them -- d being e itself, a positive power of it, a + /// product holding it, a sine, tangent, arcsine or arctangent of such a thing, or a + /// polynomial in the variable e is with no constant term -- or a disjunction every + /// side of which does. Nothing here decides what a node accepts; that stays with the + /// node, and when a complex infinity is written + /// (https://github.com/asc-community/AngouriMath/issues/217) and a quotient's domain + /// condition changes under the codomains that admit it, this follows. Anything not + /// proven keeps its condition: a false negative is a redundant clause, a false positive + /// would claim a value at a point. /// /// /// Decided on the expression as it stands, which matters: x/x provided not x = 0 @@ -216,27 +220,41 @@ private static Entity Without(Entity expression, Entity predicate) }; /// - /// Whether has a node that is undefined wherever - /// is zero. + /// Whether has no value wherever is + /// zero, by its own domain condition read in the ambient codomain + /// (): the condition excludes the zeros of + /// where a conjunct not d = 0 or d > 0 has d + /// vanishing with e, or a disjunction has every side excluding them -- + /// x^x's not x = 0 or x > 0. /// private static bool IsUndefinedAtTheZerosOf(Entity expression, Entity e) - => expression.Nodes.Any(node => node switch + => ExcludesTheZerosOf(expression.DomainConditionIn(MathS.Settings.Codomain), e); + + private static bool ExcludesTheZerosOf(Entity condition, Entity e) + => condition switch { - Divf(_, var d) => VanishesWith(d, e), - Powf(var d, var power) => VanishesWith(d, e) && (power.Evaled is Real { IsNegative: true } || VanishesWith(power, e)), - Logf(var @base, var antilogarithm) => VanishesWith(antilogarithm, e) || VanishesWith(@base, e), + Andf(var left, var right) => ExcludesTheZerosOf(left, e) || ExcludesTheZerosOf(right, e), + Orf(var left, var right) => ExcludesTheZerosOf(left, e) && ExcludesTheZerosOf(right, e), + Notf(Equalsf(var d, var zero)) when zero.Evaled is Complex { IsZero: true } => VanishesWith(d, e), + Notf(Equalsf(var zero, var d)) when zero.Evaled is Complex { IsZero: true } => VanishesWith(d, e), + Greaterf(var d, var zero) when zero.Evaled is Complex { IsZero: true } => VanishesWith(d, e), _ => false, - }); + }; /// /// Whether is zero wherever is: d is - /// e, a positive power of it, a product with such a factor, or -- for a variable - /// e -- a polynomial in it without a constant term. + /// e, a positive power of it, a product with such a factor, a sine, tangent, + /// arcsine or arctangent of such a thing, or -- for a variable e -- a polynomial + /// in it without a constant term. /// private static bool VanishesWith(Entity d, Entity e) { if (d == e) return true; + // A function that is zero at zero, of something that vanishes: `sin(x)/x` is `0/0` + // at zero. + if (d is Sinf or Tanf or Arcsinf or Arctanf) + return VanishesWith(d.DirectChildren[0], e); if (d is Powf(var @base, var power) && power.Evaled is Real { IsPositive: true }) return VanishesWith(@base, e); if (d is Mulf) diff --git a/Sources/Tests/UnitTests/Core/ProvidedImpliedByTheExpressionTest.cs b/Sources/Tests/UnitTests/Core/ProvidedImpliedByTheExpressionTest.cs index 117e14063..f7d7c71fd 100644 --- a/Sources/Tests/UnitTests/Core/ProvidedImpliedByTheExpressionTest.cs +++ b/Sources/Tests/UnitTests/Core/ProvidedImpliedByTheExpressionTest.cs @@ -13,10 +13,10 @@ namespace AngouriMath.Tests.Core { /// /// A provided condition the expression states on its own is dropped: 1/x provided - /// not x = 0 is 1/x, since the quotient has no value at zero whether or not a - /// condition says so. Only where the expression proves it -- a quotient, a negative power, a - /// logarithm, 0^0 -- and on the expression as it stands after simplification, so that - /// x/x, which becomes 1, keeps the condition it can no longer state. + /// not x = 0 is 1/x, since the quotient's own domain condition, read in the + /// ambient codomain, already excludes zero. Only where that domain condition proves it, and + /// on the expression as it stands after simplification, so that x/x, which becomes + /// 1, keeps the condition it can no longer state. /// https://github.com/asc-community/AngouriMath/issues/1394 /// [Trait("Area", "Core")] @@ -28,6 +28,8 @@ public sealed class ProvidedImpliedByTheExpressionTest [InlineData("1/x provided not x = 0", "1/x")] [InlineData("x^(-2) provided not x = 0", "1/x^2")] [InlineData("ln(x) provided not x = 0", "ln(x)")] + [InlineData("sin(x)/x + x^x provided not x = 0 and not y = 0", "sin(x)/x + x^x provided not y = 0")] + [InlineData("tan(x) provided not cos(x) = 0", "tan(x)")] [InlineData("1/(x * y) provided not x = 0 and not y = 0", "1/(x * y)")] [InlineData("1/(x^2 + x) provided not x = 0 and not x + 1 = 0", "1/(x^2 + x)")] [InlineData("1/(x^2 + x) provided not x = 0 and not y = 0", "1/(x^2 + x) provided not y = 0")] @@ -49,8 +51,8 @@ public void ADerivativeStatesItsOwnDomain(string function, string derivative) /// /// A condition the expression does not state stays: the one on a quotient that has - /// cancelled, and one about a symbol the expression no longer holds, and one about a - /// factor beside the one the quotient is by. + /// cancelled, one about a symbol the expression no longer holds, and one about a factor + /// beside the one the quotient is by. /// [Theory] [InlineData("x / x provided not x = 0")]