Definitions

<< Experimental`;
<< Developer`;
Needs[ "Utilities`FilterOptions`" ];
Needs["Graphics`FilledPlot`" ];
Off[General::spell1];
\(\(Off[$MaxExtraPrecision::meprec];\)
\)
\(\(Unprotect[Primes, Integers, Rationals, Reals, Complexes, Algebraics, 
        Booleans, Exists, ForAll];\)
\)
Format[Primes,  StandardForm] := ℙ
Format[Integers,  StandardForm] := ℤ
Format[Rationals,  StandardForm] := ℚ
Format[Reals,  StandardForm] := ℝ
Format[Complexes,  StandardForm] := ℂ
Format[Algebraics,  StandardForm] := 𝔸
\(\(\(Format[Booleans, \ StandardForm] := 𝔹\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "ℙ", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Primes", b}], StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "ℙ", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Primes", b}], InputForm]\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "ℤ", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Integers", b}], StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "ℤ", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Integers", b}], InputForm]\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "ℚ", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Rationals", b}], StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "ℚ", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Rationals", b}], InputForm]\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "ℝ", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Reals", b}], StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "ℝ", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Reals", b}], InputForm]\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "ℂ", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Complexes", b}], StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "ℂ", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Complexes", b}], InputForm]\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "𝔸", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Algebraics", b}], 
        StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "𝔸", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Algebraics", b}], InputForm]\)\(
\)
    \)\)
MakeExpression[RowBox[{a___, "𝔹", b___}], 
        StandardForm] := 
      MakeExpression[RowBox[{a, "Booleans", b}], StandardForm]
\(\(\(MakeExpression[RowBox[{a___, "𝔹", b___}], 
        InputForm] := 
      MakeExpression[RowBox[{a, "Booleans", b}], InputForm]\)\(
\)
    \)\)
\(\(\(Exists /: \ MakeBoxes[Exists[a_, b_, c_], \ StandardForm] := 
	
      RowBox[{SubscriptBox["∃", 
            RowBox[{\ MakeBoxes[a, \ StandardForm], ",", \ 
                MakeBoxes[b, \ StandardForm]}]], 
          MakeBoxes[c, \ StandardForm]}]\)\(
\)
    \)\)
\(\(\(MakeExpression[
        RowBox[{SubscriptBox["∃", \ RowBox[{a_, ",", \ b_}]], 
            c_}], \ StandardForm] := 
	
      MakeExpression[
        RowBox[{"Exists", "[", a, ",", b, ",", 
            c, "]"}], \ StandardForm]\)\(
\)
    \)\)
\(\(\(ForAll /: \ MakeBoxes[ForAll[a_, b_, c_], \ StandardForm] := 
	
      RowBox[{SubscriptBox["∀", 
            RowBox[{\ MakeBoxes[a, \ StandardForm], ",", \ 
                MakeBoxes[b, \ StandardForm]}]], 
          MakeBoxes[c, \ StandardForm]}]\)\(
\)
    \)\)
\(\(\(MakeExpression[
        RowBox[{SubscriptBox["∀", \ RowBox[{a_, ",", \ b_}]], 
            c_}], \ StandardForm] := 
	
      MakeExpression[
        RowBox[{"ForAll", "[", a, ",", b, ",", 
            c, "]"}], \ StandardForm]\)\(
\)
    \)\)
Protect[Primes, Integers, Rationals, Reals, Complexes, Algebraics, 
        Booleans, Exists, ForAll];

\(\(\(InequalityPlot[ineq_, {x_, x0_, x1_}, {y_, y0_, y1_}, 
        opts___?OptionQ] := 
	
      Module[{cyls, \ plots, \ 
          bds}, 
		cyls = \(GenericCylindricalAlgebraicDecomposition[
              ineq && x0 < x < x1 && y0 < y < y1, {x, 
                y}]\)[\([1]\)]; 
		bds = \(Boundaries /. {opts}\) /. {Boundaries -> False}; 
		plots = 
			If[cyls === False, 
            Plot[y1 + 1, {x, x0, x1}, PlotRange -> {{x0, x1}, {y0, y1}}, 
              FilterOptions[\ FilledPlot, \ opts\ ]], 
					If[
              Head[cyls] === Or, cyls = List @@ cyls, 
              cyls = {cyls}]; 
					\(cylinderplot[#, x, 
                  FilterOptions[FilledPlot, \ opts]] &\) /@ cyls]; 
		If[
          bds\  && \ cyls =!= False, \ 
          plots = {plots, 	\(boundaryplot[#, x, 
                    FilterOptions[FilledPlot, \ opts]] &\) /@ 
                cyls}]; 
	\ \ Show[\ 
          plots, \ 
\ \ \ \ \ \ FilterOptions[\ Graphics, \ 
            opts], \ 
\ \ \ \ \ \ Axes -> True, \ 
          AxesLabel -> {x, 
              y}, \ 
\ \ \ \ \ \ DisplayFunction -> $DisplayFunction, 
          AspectRatio -> Automatic, 
          PlotRange -> {{x0, x1}, {y0, y1}}\ ]]\)\(
\)
    \)\)
\(\(\(cylinderplot[cyl_, x_, opts___?OptionQ] := 
	 (*\ 
        assumes\ form\ a < x < 
            b\  && \ \((\(\(c < y < d\)\(\ \)\(||\)\)\  ... )\)\ *) 
	
      Module[{x0 = cyl[\([1, 1]\)], x1 = cyl[\([1, 5]\)], ys}, 
		ys = 
          If[Head[cyl[\([2]\)]] === Or, 
            List @@ \((cyl[\([2]\)])\), {cyl[\([2]\)]}]; 
		\(FilledPlot[\ {#[\([1]\)], #[\([5]\)]}, \ {x, \ x0, x1}, \ DisplayFunction -> Identity, 
              opts] &\) /@ ys]\)\(		\)\(
\)
    \)\)
\(boundaryplot[cyl_, x_, opts___?OptionQ] := 
	 (*\ 
        assumes\ form\ a < x < 
            b\  && \ \((\(\(c < y < d\)\(\ \)\(||\)\)\  ... )\)\ *) 
	
      Module[{x0 = cyl[\([1, 1]\)], x1 = cyl[\([1, 5]\)], ys}, 
		ys = 
          If[Head[cyl[\([2]\)]] === Or, 
            List @@ \((cyl[\([2]\)])\), {cyl[\([2]\)]}]; 
		\({Graphics[
                Line[{{x0, #[\([1]\)] /. x -> x0}, {x0, #[\([5]\)] /. 
                        x -> x0}}]], 
			Graphics[
                Line[{{x1, #[\([1]\)] /. x -> x1}, {x1, #[\([5]\)] /. 
                        x -> x1}}]], 
              Plot[\ {#[\([1]\)], #[\([5]\)]}, \ {x, \ x0, x1}, \ 
                DisplayFunction -> Identity, opts]} &\) /@ 
          ys]		\)

PlotTriangle[a_, b_, c_] := 
      With[{x = (((a^2) + (b^2) - (c^2))/(2 a)), 
          y = (Sqrt[(b^2) - (((((a^2) + (b^2) - (c^2)))^2)/(4 (a^2)))])}, 
        Show[Graphics[Polygon[{{0, 0}, {a, 0}, {x, y}, {0, 0}}], 
            PlotRange -> All, AspectRatio -> Automatic, Axes -> False, 
            DefaultColor -> RGBColor[0.7, 0.7, 0.5]]]]

Infimum = Experimental`PolynomialMinValue;

Solving Inequalities and Using Assumptions

Inequalities

Solving systems of polynomial equations and inequalities

Mathematica 3.5 contains several new functions allowing to solve systems of polynomial equations and inequalities.

What does it mean to "solve" a system of equations and inequalities.

ineqs = (((x + (7/4)))^2) + (((y - (9/4)))^2) < 
          (1/9) || (((x - (9/4)))^2) + (((y - (9/4)))^2) < (1/9) || 
        (x^2) + (y^2) < 25 && (((x - 2))^2) + (((y - 2))^2) > 
            1 && (((x + 2))^2) + (((y - 2))^2) > 
            1 && ((x^2) + (((y + 1))^2) > 5 || 
              (x^2) + (((y - 1))^2) < 9); 
    InequalityPlot[ineqs, {x, -5, 5}, {y, -5, 5}]

Decide whether the system has any solutions, and if yes find one.

Experimental`ExistsRealQ[ineqs, vars] whether there exist real values of vars satisfying the system of polynomial equations and inequalities ineqs.
Experimental`ForAllRealQ[ineqs, vars] whether the system of polynomial equations and inequalities ineqs is satisfied for all real values of vars.
Developer`InequalityInstance[ineqs, vars] finds a real solution of the system of polynomial equations and inequalities ineqs.

ExistsRealQ[ineqs,  {x,  y}]

InequalityInstance[ineqs,  {x, y}]

Conjecture by T.Ono (1914). Counterexample G.Quijano (1915). Proof for acute triangles F.Balitrand (1916).

\(\(\(	\)\(OnoIneq = 
      27\ \((b\^2 + c\^2 - a\^2)\)\^2\ \((a\^2 + c\^2 - b\^2)\)\^2\ \((a\^2 + b\^2 - c\^2)\)\^2 ≤ \((4\ F)\)\^6; 
    F = \@\(s\ \((s - a)\)\ \((s - b)\)\ \((s - c)\)\); \ 
    s = \(1\/2\) \((a + b + c)\); \ 
    triangle = 
      a > 0 && b > 0 && c > 0 && a + b > c && b + c > a && a + c > b; 
    acute = a\^2 + b\^2 > c\^2 && b\^2 + c\^2 > a\^2 && 
        a\^2 + c\^2 > b\^2;\)\)\)

Timing[
      InequalityInstance[! (Implies[triangle, 
              OnoIneq]), {a, b, c}]]

PlotTriangle[3/4, 1/2, 1]

Timing[
      ForAllRealQ[Implies[triangle && acute, OnoIneq], {a, b, c}]]

Describe the solution set using inequalities in a more useful "cylindrical" form

Experimental`CylindricalAlgebraicDecomposition[ineqs, {(Subscript[x, 1]),…,(Subscript[x, n])}] finds a decomposition of the solution set of polynomial equations and inequalities ineqs into cylindrical parts whose directions correspond to the successive (Subscript[x, i]).
Experimental`GenericCylindricalAlgebraicDecomposition[ineqs, {(Subscript[x, 1]),…,(Subscript[x, n])}] finds a pair of sets A nad B, such that the solution set of polynomial inequalities ineqs is contained between A\B and A⋃B, A consists of open cells cylindrical in directions corresponding to the successive (Subscript[x, i]), and B is a hypersurface described by a system of equations.

By cylindrical form of inequalities we mean the following form

\(TextForm\`l\_1 ≺ x\_1 ≺ 
          u\_1 && \(l\_2\) \((x\_1)\) ≺ 
          x\_2 ≺ \(u\_2\) \((x\_1)\) && … && \(l\_n\) \((x\_1, …\ , x\_\(n - 1\))\) ≺ 
          x\_n ≺ \(u\_n\) \((x\_1, …\ , 
              x\_\(n - 1\))\) || …\)

\(TextForm\`where\ \(l\_i\) and\ \(u\_i\) are\ algebraic\ functions, \ 
    and\  ≺ \ 
      is\ one\ of\ \ \(\({\(<\)\(\(,\)\(\(≤\)\(\(,\)\(==\)\)\)\)\ }\)\(.\)\)\)

ineq1 = (x^2) + (y^2) ≤ 1;

InequalityPlot[ineq1, {x, -1, 1}, {y, -1, 1}];

CylindricalAlgebraicDecomposition[ineq1, {x, y}]

GenericCylindricalAlgebraicDecomposition[ineq1, {x, y}]

ineq2 = 
        (x^2) + x y + (y^2) < 1 && 
          (x^2) - x y + (y^2) ≥ (1/4);

InequalityPlot[ineq2, {x, -5/4, 5/4}, {y, -5/4, 5/4}, 
        Boundaries -> True];

CylindricalAlgebraicDecomposition[ineq2, {x, y}]

GenericCylindricalAlgebraicDecomposition[ineq2, {x, y}]

ineq3 = 0 < (x^2) + (y^2) < 1;

CylindricalAlgebraicDecomposition[ineq3, {x, y}]

GenericCylindricalAlgebraicDecomposition[ineq3, {x, y}]

Eliminate variables from the system ==
Compute projections of the solution set ==
Eliminate quantifiers wrt. some of the variables.

Exists[vars, assumptions, expr] existential quantifier. (There exist values of vars satisfying assumptions such that expr is true.)
ForAll[vars, assumptions, expr] general quantifier. (For all values of vars satisfying assumptions expr is true.)
Experimental`Resolve[expr] attempts to eliminate quantifiers in expr.

The current version of Resolve can eliminate quantifiers from real polynomial equation and inequality systems. In general case it uses an algorithm based on Collins' cylindrical algebraic decomposition algorithm, with special case versions of this algorithm for decision problems and for strong inequalities. For the linear quantifier elimination it uses the Loos-Weispfenning algorithm, and for linear decision problem a method based on the simplex algorithm. When equations form a zero dimensional ideal Groebner bases are used.

Resolve[ (Subscript[∃ , x, x ∈ ℝ])(x^2) - 
            x + 1 < 0 ]

Resolve[ (Subscript[∀ , {x, y}, (x^2) + (y^2) < 1])(((x - 2))^2) + (((y - 2))^2) > 3 ]

Resolve[ (Subscript[∃ , x, (x | (Subscript[a, 0]) | (Subscript[a, 1]) | (Subscript[a, 2])) ∈ ℝ])(Subscript[a, 2]) (x^2) + (Subscript[a, 1]) x + (Subscript[a, 0]) == 0 ]

Resolve[ (Subscript[∃ , x, (x | a | b) ∈ ℝ])(x^6) + a x + b == 0 ]

Resolve[ (Subscript[∀ , ϵ, ϵ > 0])(Subscript[∃ , M, M ∈ ℝ])(Subscript[∀ , x, x > M && λ ∈ ℝ])-ϵ < ((3 (x^2) - 5 x + 7)/(7 (x^2) - 2 x + 11)) - λ < ϵ ]

Constrained minimization of polynomials

Experimental`Minimize[f, constr, vars] finds the infimum of values of f on the set of points satisfying equation and inequality constraints constr, and a point at which the infimum is attained, if such point exists.
Experimental`Infimum[f, constr, vars] finds the infimum of values of f on the set of points satisfying equation and inequality constraints constr.

butterfly = 
        InequalityPlot[
          (x^4) + (y^4) ≤ (x^2), {x, -(5/4), 
            (5/4)}, {y, -(3/4), (3/4)}];

Minimize[-(x^2) - (y^2), 
      (x^4) + (y^4) ≤ (x^2), {x, y}]

Show[butterfly, 
      Graphics[{RGBColor[1, 0, 0], PointSize[0.03],  
          Point[{x, y} /. %[[2]]]}]]

M.S.Klamkin, D.J.Newman, C.C.Rousseau, D.Shanks, SIAM Review 14 (1972).
Find values of k for which the following inequality is true for all a, b, c sides of a triangle.

KNRS = 
        (a^3) + (b^3) + (c^3) ≥ 
          3 a b c + k (a - b) (b - c) (c - a);

triangle = 
        a > 0 && b > 0 && c > 0 && a + b > c && b + c > a && 
          a + c > b;

Infimum[k, k > 0  &&  triangle  &&  ! KNRS, {a, b, c, k}] // 
      Timing

ToRadicals[%[[2]]]

Implementation

In the general case we use algorithms based on the Cylindrical Algebraic Decomposition algorithm, with the recent improvements of projection operator by McCallum. We recognize several special cases where we can use specialized algorithms. If all polynomials are linear we use algorithms based on a modification of the Simplex optimization algorithm (for decision problem with rational or inexact numeric coefficients), or on the Loos-Weispfenning linear quantifier elimination algorithm. If the system contains only strong inequalities we use a version of the CAD algorithm with a simpler projection operator and we lift only full dimensional cells. If the equations form a zero-dimensional complex ideal we use Groebner bases. Also, if polynomials are linear in some variables we use the Loos-Weispfenning linear quantifier elimination algorithm as a preprocessor.

Assumptions

In Mathematica V3.1 one can specify assumptions about variables or patterns to be used by Simplify, FullSimplify, and FunctionExpand.

There are three types of assumptions that can be used:

Set Membership Assumptions

Element[x, set] or x ∈ set asserts that x is an element of set.
Element[{(Subscript[x, 1]),…,(Subscript[x, n])}, set] asserts that all the (Subscript[x, i]) are elements of set.
Element[patt, set] asserts that any expression matching the pattern patt is an element of set.

The available set names are: Primes (ℙ), Integers (ℤ), Rationals (ℚ), Reals (ℝ), Complexes (ℂ), Algebraics (𝔸), and Booleans (𝔹).

149 ∈ ℙ

(2^((Sqrt[3]))) ∈ 𝔸

Assumptions can be given as a second argument to Simplify, FullSimplify, and FunctionExpand.

Simplify[Sin[n π], 
      n ∈ ℤ]

Simplify[
      PolyLog[Gamma[
            Round[x]^2 + 
              1], (E^x)] ∈ ℝ, 
      x ∈ ℝ]

The condition tested here is that the first argument of PolyLog be an integer, and that the second argument be a real number.

FunctionExpand[
      EulerPhi[(p^2) (q^3)], (p | q) ∈ ℙ && 
        p ≠ q]

Inequality Assumptions

Simplify[(Sqrt[(x^2) + 2 x y + (y^2)]), x > -y]

FunctionExpand[Log[a x],  a > 0]

Simplify[
      BesselJ[x + y, 
          (x^2) - x y + (y^2) + 1] ∈ ℝ, (x | 
            y) ∈ ℝ]

The condition tested here is that the first argument is real and the second is positive.

Simplify[((((a^Erf)[b]))^c), 
      b ∈ ℝ]

Simplify[((((a^(((9 Erf[b])/8)))))^c), 
      b ∈ ℝ]

Here the "middle" power has to be between -1 and 1.

((((a^(((9 Erf[b])/8)))))^c) - 
        (a^(((9 Erf[b])/8) c)) /. {a -> -1, b -> 3. , 
        c -> I}

Equation Assumptions

Simplify[Expand[((((x^2) - 3 y + 2))^2) (((x + 5 y))^3)], 
      (x^2) == 3 y]

Direct access to the assumptions mechanism

Experimental`ImpliesQ[(Subscript[expr, 1]),(Subscript[expr, 2])] tests whether the expression (Subscript[expr, 1]) implies (Subscript[expr, 2]). If cannot determine whether (Subscript[expr, 1]) implies (Subscript[expr, 2]) returns False.

ImpliesQ[x > 0 && y ∈ ℝ, 
      CosIntegral[(x^y)] ∈ ℝ]

ImpliesQ[(x^4) + (y^4) < E, 
      x - y < ((((Sqrt[2])))^π)]

ImpliesQ[
      x ∈ ℝ, (E^x) ≥ x + 1]

Implementation

To prove that a given statement follows from assumptions we use algorithms for deciding the existence of solutions of polynomial equation and inequality systems, together with a collection of inequalities involving non-polynomial functions, and a database of relations allowing to derive set membership of the function's value based on conditions satified by its arguments.