Skip to content

Over the reals, answer an exponential equation with real roots only #2433

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Rafael-SOWNet wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Over the reals, answer an exponential equation with real roots only #2433

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions BREAKING-CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -374,6 +374,32 @@ included; a two-sided limit at a finite point is not changed. Found by limitchec
| `"x * (ln(-tanh(x)) + 1)".ToEntity().Limit("x", 0, ApproachFrom.Left)` | `0` in 3.2 s | `0` in 0.44 s |
| `"sin(x) * (ln(-tanh(x)) + 1/x)".ToEntity().Limit("x", 0, ApproachFrom.Left)` | `1` in 3.7 s | `1` in 1.1 s |

### Over the reals, an exponential equation has no root where the power would have to be non-positive

**Silent: under `MathS.Settings.Codomain.Set(Domain.Real)`, a root that is a logarithm of a number that is not a
positive real is dropped.** A positive base to a real power is positive, so `a^u = v` has a real `u` only for a
positive `v`, and `ln(-1)` is `i pi`. Decided on an enclosure of `v`'s value, so a `v` that cannot be told from the
positive reals keeps its root, and a symbolic one keeps it as before (`e^x = y` is still `{ ln(y) }`). An equation
solved through a replacement that is real at every real `x`, such as `x^2`, and whose replacement has no real root,
has none either. A replacement that is not real at a real `x`, such as `i x`, is solved over the complex numbers,
so `e^(i x) = -1` keeps its root `pi`. The default complex codomain is not changed.
[#2425](https://github.com/asc-community/AngouriMath/issues/2425)

| Input, with `Codomain` set to `Domain.Real` | Was (2.6.0) | Now |
|---|---|---|
| `"e^x + 1 = 0".Solve("x")` | `{ ln(-1) }` | `{ }` |
| `"e^x - 2e^(-x) - 1 = 0".Solve("x")` | `{ ln(-1), ln(2) }` | `{ ln(2) }` |
| `"2^x = -3".Solve("x")` | `{ log(2, -3) }` | `{ }` |
| `"(1/2)^x = -4".Solve("x")` | `{ log(1/2, -4) }` | `{ }` |
| `"3 e^x + 5 = 0".Solve("x")` | `{ ln(-5/3) }` | `{ }` |
| `"e^(2x + 1) = -3".Solve("x")` | `{ (ln(-3) - 1) / 2 }` | `{ }` |
| `"e^(2x) + e^x - 2 = 0".Solve("x")` | `{ 0, ln(-2) }` | `{ 0 }` |
| `"e^x + e^(-x) = 1".Solve("x")` | `{ ln((1 - sqrt(-3)) / 2), ln((1 + sqrt(-3)) / 2) }` | `{ }` |
| `"e^x - e^(-x) = 3".Solve("x")` | `{ ln((3 - sqrt(13)) / 2), ln((3 + sqrt(13)) / 2) }` | `{ ln((3 + sqrt(13)) / 2) }` |
| `"e^x = -1 + i".Solve("x")` | `{ ln(-1 + i) }` | `{ }` |
| `"e^(x^2) = -1".Solve("x")` | `{ sqrt(ln(-1)), -sqrt(ln(-1)) }` | `{ }` |
| `"e^(x^2) + e^(-x^2) = 1".Solve("x")` | `{ sqrt(ln((1 - sqrt(-3)) / 2)), -sqrt(ln((1 - sqrt(-3)) / 2)), sqrt(ln((1 + sqrt(-3)) / 2)), -sqrt(ln((1 + sqrt(-3)) / 2)) }` | `{ }` |

### An equation through a negative whole power is not answered with no roots

**Silent: an empty answer becomes the roots.** Inverting `x^n = v` for a negative whole `n` multiplied by the roots
Expand Down
22 changes: 20 additions & 2 deletions Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/AnalyticalEquationSolver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -318,6 +318,7 @@ bool ProductIsDefinedAt(Entity root)
var newVar = Variable.CreateTemp(expr.Vars);
// Here we find all possible replacements and find one that has at least one solution
Set? unsettled = null;
var noRealReplacement = false;
foreach (var alt in SpellingsToSolveOver(expr))
{
MultithreadingFunctional.ExitIfCancelled();
Expand All @@ -328,8 +329,23 @@ bool ProductIsDefinedAt(Entity root)
var minimumSubtree = TreeAnalyzer.GetMinimumSubtree(alt, x);
if (minimumSubtree == x)
continue;
// Here we are trying to solve for this replacement
var solutionsSet = Solve(alt.Substitute(minimumSubtree, newVar), newVar).InnerSimplified;
// Here we are trying to solve for this replacement. Over the reals the
// replacement is real only where the subtree it stands for is real at every
// real x: i x is not, and e^u = -1 has the real root pi for u = i x. Where it
// is not, the replacement is solved over the complex numbers, and the roots
// in x are read over the reals when they are solved for below.
// https://github.com/asc-community/AngouriMath/issues/2425
// Where it is, a replacement with no real root is an x with none: e^(x^2) = -1.
Entity solutionsSet;
var readOverTheReals = MathS.Settings.Codomain.Value == Core.Domain.Real;
var realReplacement = readOverTheReals && TreeAnalyzer.IsRealValued(minimumSubtree, x);
if (readOverTheReals && !realReplacement)
using (MathS.Settings.Codomain.Set(Core.Domain.Complex))
solutionsSet = Solve(alt.Substitute(minimumSubtree, newVar), newVar).InnerSimplified;
else
solutionsSet = Solve(alt.Substitute(minimumSubtree, newVar), newVar).InnerSimplified;
if (realReplacement && solutionsSet is FiniteSet { IsSetEmpty: true })
noRealReplacement = true;
if (solutionsSet is FiniteSet { IsSetEmpty: false } enums)
{
var solutions = enums.Select(solution => Solve(minimumSubtree - solution, x, compensateSolving: true)).Unite().InnerSimplified;
Expand All @@ -346,6 +362,8 @@ bool ProductIsDefinedAt(Entity root)
}
if (unsettled is { } condition)
return condition;
if (noRealReplacement)
return Set.Empty;
// // //
}

Expand Down
34 changes: 34 additions & 0 deletions Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/InvertNode.Classes.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,12 +127,46 @@ partial record Powf
: null;
return principal;
}
// Over the reals a positive base to a real power is positive, so a value that is not
// a positive real is no power of it: e^x = -1 has no real root, and log(e, -1) is
// i pi. https://github.com/asc-community/AngouriMath/issues/2425
if (MathS.Settings.Codomain.Value == Core.Domain.Real && IsNotAPowerOverTheReals(value, x))
return Enumerable.Empty<Entity>();
// a ^ x = value => x = log(a, value)
// TODO: determine how we should return periodic roots as
// (e ^ x) ^ a != (e ^ a) ^ x for logs
return Exponent.Invert(MathS.Log(Base, value), x);
}

/// <summary>
/// Whether, for a positive real base and an exponent real at every real
/// <paramref name="x"/>, <paramref name="value"/> is decidedly not a positive real.
/// </summary>
/// <remarks>
/// Decided on an enclosure of the value, never on its printed form: <c>ln(-1)</c> stays
/// a node, and only its value says it is <c>i pi</c>. A value is not a positive real
/// where its imaginary part is enclosed away from zero, where its real part is enclosed
/// below zero whatever its imaginary part is, or where it is exactly zero. Anything
/// else -- a value the enclosure cannot separate from the positive reals, or one with a
/// free variable -- is left to the inversion as before, so this only ever removes a
/// root it has proved is not one.
/// </remarks>
private bool IsNotAPowerOverTheReals(Entity value, Entity x)
{
if (x is not Variable variable || value.ContainsNode(x)
|| !TreeAnalyzer.IsRealValued(Exponent, variable)
|| Numerics.PreciseEvaluation.Of(Base, EnclosureDigits) is not { } @base
|| !@base.Im.IsZero || @base.Re.Low.Sign <= 0)
return false;
if (value.Evaled is Integer { IsZero: true })
return true;
if (Numerics.PreciseEvaluation.Of(value, EnclosureDigits) is not { } enclosure)
return false;
return enclosure.Im.Mignitude.Sign > 0 || enclosure.Re.High.Sign < 0;
}

private const int EnclosureDigits = 40;

// The principal power z^p is e^(p ln z), so its argument is p arg(z): in (-p pi, p pi]
// for 0 < p < 1, and in [p pi, -p pi) for -1 < p < 0, where it is never 0. A value
// outside that sector is no power of anything, and v^(1/p) is then a number whose
Expand Down
49 changes: 49 additions & 0 deletions Sources/Tests/UnitTests/Common/SolverRegressionTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,5 +243,54 @@ public void Issue812_ASymbolicRightHandSideCarriesTheCondition()
var printed = "abs(x) = a".ToEntity().Solve("x").Stringize();
Assert.Contains("a >= 0", printed);
}
// https://github.com/asc-community/AngouriMath/issues/2425
// Over the reals a positive base to a real power is positive, so e^x = t has a real
// root only for a positive t. e^x + 1 = 0 was answered { ln(-1) }, which is i pi, and
// e^x - 2e^(-x) - 1 = 0, a quadratic in e^x with the roots 2 and -1, kept ln(-1) beside
// ln(2). Each root is checked to be real and to satisfy the equation, and the count says
// that none was lost.
[Theory]
[InlineData("e^x + 1 = 0", 0)]
[InlineData("3 e^x + 5 = 0", 0)]
[InlineData("2^x = -3", 0)]
[InlineData("e^(2x + 1) = -3", 0)]
[InlineData("e^x - 2e^(-x) - 1 = 0", 1)]
[InlineData("e^(2x) + e^x - 2 = 0", 1)]
[InlineData("e^x - e^(-x) = 3", 1)]
[InlineData("e^x + e^(-x) = 1", 0)]
[InlineData("e^x + e^(-x) = 3", 2)]
[InlineData("e^(2x) - 3e^x + 2 = 0", 2)]
[InlineData("e^(x^2) = -1", 0)]
[InlineData("e^(x^2) + e^(-x^2) = 1", 0)]
// A replacement that is not real at a real x is solved over the complex numbers:
// e^(i x) = -1 has the real root pi.
[InlineData("e^(i x) = -1", 1)]
public void Issue2425_AnExponentialEquationOverTheRealsHasOnlyRealRoots(string equation, int count)
{
using var _ = MathS.Settings.Codomain.Set(AngouriMath.Core.Domain.Real);
var statement = (Entity.Equalsf)equation.ToEntity();
var roots = Assert.IsType<Entity.Set.FiniteSet>(statement.Solve("x"));
Assert.Equal(count, roots.Count);
foreach (var root in roots)
{
var value = Assert.IsAssignableFrom<Entity.Number.Complex>(root.Evaled);
Assert.True(value.ImaginaryPart.EDecimal.Abs().CompareTo(PeterO.Numbers.EDecimal.FromString("1E-30")) < 0,
$"{root} = {value} is not real");
var residual = Assert.IsAssignableFrom<Entity.Number.Complex>(
(statement.Left - statement.Right).Substitute("x", root).Evaled);
Assert.True(residual.Abs().EDecimal.CompareTo(PeterO.Numbers.EDecimal.FromString("1E-30")) < 0,
$"{root} leaves {residual}");
}
}

// The complex reading is untouched: e^x + 1 = 0 has the root i pi there.
[Fact]
public void Issue2425_OverTheComplexNumbersTheRootIsKept()
{
var statement = (Entity.Equalsf)"e^x + 1 = 0".ToEntity();
var root = Assert.Single(Assert.IsType<Entity.Set.FiniteSet>(statement.Solve("x")));
var value = Assert.IsAssignableFrom<Entity.Number.Complex>(root.Evaled);
Assert.Equal(System.Math.PI, value.ImaginaryPart.EDecimal.ToDouble(), 12);
}
}
}
Loading