1
$\begingroup$

For a proof, I'm working with a polynomial $p(x,m)$ and I need to show that: For any $m\in (0,6)$, $p_m(x)\equiv p(x,m)$ has a unique real root in $(0,1/2)$. I find that this is true by using Reduce in Mathematica, but I need to understand how to prove it.

Ideally, I'd like to go through the step-by-step process that the Reduce command does, but I haven't been able to understand it (I tried running trace on the Reduce command but the output is impossible for me to understand).

The polynomial $p$ is named "auxpoly" in the code below.

P1[x_, m_] := 
 2 (-6 + m) m^8 (-27 + 2 m) - 
  x (-15930 m^7 + 5451 m^8 + 1158 m^9 - 236880 m^6 x + 87728 m^7 x + 
     46144 m^8 x - 1482048 m^5 x^2 + 616128 m^6 x^2 + 
     703888 m^7 x^2 - 4460544 m^4 x^3 + 2058112 m^5 x^3 + 
     6162880 m^6 x^3 - 6414336 m^3 x^4 + 2120192 m^4 x^4 + 
     34435712 m^5 x^4 - 3538944 m^2 x^5 - 5603328 m^3 x^5 + 
     124934656 m^4 x^5 - 16908288 m^2 x^6 + 289193984 m^3 x^6 - 
     12582912 m x^7 + 407371776 m^2 x^7 + 314572800 m x^8 + 
     100663296 x^9)

P2[x_, m_] := -1836 m^7 + 586 m^8 + 52 m^9 + 
  4 x (-11808 m^6 + 4200 m^7 + 1528 m^8 - 103752 m^5 x + 
     40891 m^6 x + 33098 m^7 x - 398592 m^4 x^2 + 181024 m^5 x^2 + 
     358416 m^6 x^2 - 691200 m^3 x^3 + 303424 m^4 x^3 + 
     2375360 m^5 x^3 - 442368 m^2 x^4 - 319488 m^3 x^4 + 
     10032448 m^4 x^4 - 1720320 m^2 x^5 + 26613760 m^3 x^5 - 
     1572864 m x^6 + 42270720 m^2 x^6 + 36175872 m x^7 + 12582912 x^8)

auxpoly[x_, m_] := (P1[x, m])^2 - 2 x *(m + 2 x)*(P2[x, m]^2)

When I run the Reduce command as follows, I find that for each $m$, there is a single real root in the interval $(0,1/2)$. I confirm the result by plotting CountRoots for each $m$.

Reduce[auxpoly[x, m] == 0 && x > 0 && x <= 1/2 && m > 0 && m < 6, x]

Screenshot of output

$\endgroup$
3
  • $\begingroup$ Since you desire a step-by-step solution, why not posting this question on math.stackexchange? $\endgroup$
    – yarchik
    Jun 25, 2020 at 6:12
  • $\begingroup$ The code involved uses some heavy machinery such as cylindrical algebraic decomposition (CAD). It will not readily lend itself to human-understandable step-by-step. One can obtain a computer-assisted proof using Discriminant, Roots, and some related functions, but it is not obvious whether that will suit the needs of s-o-s. $\endgroup$ Jun 25, 2020 at 13:42
  • $\begingroup$ Thanks @DanielLichtblau, that's helpful! $\endgroup$
    – ilan
    Jun 26, 2020 at 5:25

1 Answer 1

1
$\begingroup$
Clear["Global`*"]

P1[x_, m_] := 
 2 (-6 + m) m^8 (-27 + 2 m) - 
  x (-15930 m^7 + 5451 m^8 + 1158 m^9 - 236880 m^6 x + 87728 m^7 x + 
     46144 m^8 x - 1482048 m^5 x^2 + 616128 m^6 x^2 + 703888 m^7 x^2 - 
     4460544 m^4 x^3 + 2058112 m^5 x^3 + 6162880 m^6 x^3 - 6414336 m^3 x^4 + 
     2120192 m^4 x^4 + 34435712 m^5 x^4 - 3538944 m^2 x^5 - 5603328 m^3 x^5 + 
     124934656 m^4 x^5 - 16908288 m^2 x^6 + 289193984 m^3 x^6 - 
     12582912 m x^7 + 407371776 m^2 x^7 + 314572800 m x^8 + 100663296 x^9)

P2[x_, m_] := -1836 m^7 + 586 m^8 + 52 m^9 + 
  4 x (-11808 m^6 + 4200 m^7 + 1528 m^8 - 103752 m^5 x + 40891 m^6 x + 
     33098 m^7 x - 398592 m^4 x^2 + 181024 m^5 x^2 + 358416 m^6 x^2 - 
     691200 m^3 x^3 + 303424 m^4 x^3 + 2375360 m^5 x^3 - 442368 m^2 x^4 - 
     319488 m^3 x^4 + 10032448 m^4 x^4 - 1720320 m^2 x^5 + 26613760 m^3 x^5 - 
     1572864 m x^6 + 42270720 m^2 x^6 + 36175872 m x^7 + 12582912 x^8)

auxpoly[x_, m_] := (P1[x, m])^2 - 2 x*(m + 2 x)*(P2[x, m]^2)

There are four real roots for 0 <= m <= 6

sol = Solve[{auxpoly[x, m] == 0, 0 <= m <= 6}, x, Reals];

Length@sol

(* 4 *)

However, only one of these roots is in the interval 0 <= x <= 1/2

sol2 = Solve[{auxpoly[x, m] == 0, 0 <= m <= 6, 0 <= x <= 1/2}, x, Reals];

Length@sol2

(* 1 *)

The maximum value of x is

max = NMaximize[{Normal[x /. sol2[[1]]], 0 < m < 6}, m]

(* {0.161383, {m -> 0.493441}} *)

Plotting the root as a function of m

Plot[x /. sol2, {m, 0, 6}, Epilog ->
  {Red, AbsolutePointSize[4], Point[{max[[2, 1, -1]], max[[1]]}]},
 AxesLabel -> (Style[#, 12, Bold] & /@ {m, x})]

enter image description here

$\endgroup$
2
  • $\begingroup$ Thanks very much, Bob! Do you know if it's possible to get the step-by-step process that the Solve command performs to get this result? That would be super helpful. $\endgroup$
    – ilan
    Jun 25, 2020 at 4:53
  • $\begingroup$ For very simple problems (not the one that you have) you can use WolframAlpha, e.g., WolframAlpha["solve x^3+x^2+1==0 over reals", {{"ResultOverTheReals", 2}, "Content"}, PodStates -> {"ResultOverTheReals__Step-by-step solution"}]. However, these are not the steps used by Solve. $\endgroup$
    – Bob Hanlon
    Jun 25, 2020 at 18:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.