0
$\begingroup$

I have a quite complicated function of 2 variables:

f[n_, dj_] = 
  (6*(2 - n + dj*(5 + 2*n))*(7 + n + dj*(5 + 2*n))*(-965 + 
  2*dj^4*(5 + 2*n)^4 + dj^3*(5 + 2*n)^3*(35 + 2*n) - 
  9*dj^2*(5 + 2*n)^2*(-19 + n + 2*n^2) + 
  dj*(-1 + 2*n)*(5 + 2*n)*(-73 + n*(-26 + 11*n)) - 
  n*(473 + n*(111 + n*(-37 + 8*n)))))/((5 - n + 
  dj*(5 + 2*n))*(1 - 5*n + dj*(33 + 6*n + 4*dj*(5 + 2*n)))*
  Sqrt[(5 + 2*n)^2*(5 - n + dj*(5 + 2*n))*(1 - 5*n + 
    dj*(33 + 6*n + 4*dj*(5 + 2*n)))*(2477 + 12*dj^4*(5 + 2*n)^4 + 
    4*dj^3*(5 + 2*n)^3*(59 + 2*n) - 
    dj^2*(5 + 2*n)^2*(-1573 + 4*n*(1 + 5*n)) + 
    n*(-2230 + n*(-411 + 4*n*(29 + 8*n))) - 
    2*dj*(5 + 2*n)*(-1937 + n*(435 + 2*n*(87 + 8*n))))])

I want to show that this function is always less than 1 for $n \geq d_j \geq 1$. Indeed when I do

Resolve[ForAll[{n, dj}, n >= dj >= 1, f[n, dj] < 1]]

I get True. I'm just wondering if there's a way I could show this more rigorously (i.e. "by hand," or ask Mathematica to show steps it used to get True), since I need to put this in a paper.

Improve this question
$\endgroup$
7
  • $\begingroup$ Duplicate: mathematica.stackexchange.com/q/148/5 $\endgroup$
    – rm -rf ♦
    Commented Mar 15, 2013 at 20:21
  • 1
    $\begingroup$ Are you genuinely interested in the mathematical details or are you looking for some additional reassurance of correctness? In the latter case, perhaps a plot would be useful. $\endgroup$
    – Mark McClure
    Commented Mar 15, 2013 at 20:31
  • $\begingroup$ I guess the former case. I really believe it's true. Just not sure if just showing that Mathematica says so would convince other people (for publication, for example). $\endgroup$
    – Art
    Commented Mar 15, 2013 at 20:41
  • $\begingroup$ Quoting from the answer rm linked to, "how Mathematica does things doesn't necessarily correspond to "manual" methods". Even if you knew the steps Mathematica does internally, in the majority of cases this would not be useful at all. What I'd do for publishing this is that I'd verify the result numerically and mention it that it agrees with what Mathematica told me. I would not trust Mathematica alone on this, but a numerical verification would convince me. $\endgroup$
    – Szabolcs
    Commented Mar 15, 2013 at 21:21
  • $\begingroup$ If you are looking for a computed-aided proof, I would suggest looking into the subject of "quantifier elimination." $\endgroup$
    – James Rohal
    Commented Mar 15, 2013 at 21:30

1 Answer 1

Reset to default
4
$\begingroup$

You can do most of it "by hand". With f[n_, dj_] defined as you have it, try to work with the square.

tf = Together[f[n, dj]^2];

Now group factors of numerator with factors of denominator. This happens to work because there are the same number of each and, in order, they go wll together.

Partition[
 Riffle[Apply[List, Numerator[tf]], Apply[List, Denominator[tf]]], 2]

(* Out[312]= {
{36, (5 + 2 n)^2}, 

{(2 + 5 dj - n + 2 dj n)^2, (5 + 5 dj - n + 2 dj n)^3},

{(7 + 5 dj + n + 2 dj n)^2,
    (1 + 33 dj + 20 dj^2 - 5 n + 6 dj n + 8 dj^2 n)^3},

{(-965 + 365 dj + 
    4275 dj^2 + 4375 dj^3 + 1250 dj^4 - 473 n - 454 dj n + 
    3195 dj^2 n + 5500 dj^3 n + 2000 dj^4 n - 111 n^2 - 555 dj n^2 + 
    54 dj^2 n^2 + 2400 dj^3 n^2 + 1200 dj^4 n^2 + 37 n^3 - 
    16 dj n^3 - 396 dj^2 n^3 + 400 dj^3 n^3 + 320 dj^4 n^3 - 8 n^4 + 
    44 dj n^4 - 72 dj^2 n^4 + 16 dj^3 n^4 + 32 dj^4 n^4)^2, 
  2477 + 19370 dj + 39325 dj^2 + 29500 dj^3 + 7500 dj^4 - 2230 n + 
   3398 dj n + 31360 dj^2 n + 36400 dj^3 n + 12000 dj^4 n - 411 n^2 - 
   3480 dj n^2 + 5712 dj^2 n^2 + 15360 dj^3 n^2 + 7200 dj^4 n^2 + 
   116 n^3 - 856 dj n^3 - 416 dj^2 n^3 + 2368 dj^3 n^3 + 
   1920 dj^4 n^3 + 32 n^4 - 64 dj n^4 - 80 dj^2 n^4 + 64 dj^3 n^4 + 
   192 dj^4 n^4}
} *)

It is easy to see that for all but the final pair, the numerator term will be positive and less in magnitude than its corresponding denominator term. I suspect that last pair is also amenable to analysis by hand, albeit it will be a bit more painstaking.

Improve this answer
$\endgroup$

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