0
$\begingroup$

I'm working with an expression that seems to be non-positive, but I'm having a hard time verifying it:

f1[λ_, 
  n_] := (1/
    64) (-64 - (8 λ (-4 + 
         2 r + λ + (-2 + r) r λ + 
         2 λ^2 + λ^3) ((-2 + r)^4 + (2 - r)^
          n (1 + λ)^(
          4 - n)) (5 + (-4 + r) r + λ (2 + λ)))/((-2 +
          r)^4 r (1 + λ)^3 (-1 + ((2 - r)/(1 + λ))^
         n)) + 64 (1 - ((-1 + λ)^2 (((2 - r)/(1 + λ))^
            n + (-2 + r)^2/(1 + λ)^2))/((-2 + 
            r) r (-1 + ((2 - r)/(1 + λ))^
            n))) (1 + ((-1 + λ) (1 + λ) (((2 - 
                r)/(1 + λ))^
            n + (-2 + r)^2/(1 + λ)^2))/((-2 + 
            r) r (-1 + ((2 - r)/(1 + λ))^n))) + (4 (-1 + 
         r + λ) (-4 + 
         2 r + λ + (-2 + r) r λ + 
         2 λ^2 + λ^3) (1 + (-2 + 
            r)^2/(1 + λ)^2) (-(-2 + r)^(2 n) (1 + λ)^(
          8 - 2 n) (-20 + 
            2 r (13 + (-6 + r) r) + λ + (-2 + 
               r) r λ + 2 λ^2 + λ^3) + (-2 + 
            r)^7 (10 + 2 (-4 + r) r + 6 λ + 
            r (5 + (-4 + r) r) λ + 
            2 (4 + r) λ^2 + (6 + r) λ^3 + 
            2 λ^4) + (2 - r)^(2 + n) (1 + λ)^(
          2 - n) ((-2 + 
              r)^4 - (1 + λ)^4) (-(-4 + n) (-2 + 
               r)^2 λ - (-4 + 
               n) λ (1 + λ)^2 - 
            2 (-2 + r) (1 + λ) (-3 + n + λ))))/((2 - 
         r)^7 (1 + λ)^3 (3 - r + λ) (r - 
         r ((2 - r)/(1 + λ))^n)^2) + 
    4 (-4 λ + (2 (1 + λ) (2 + ((-2 + r) (-4 - 
                 2 r (-1 + λ) + r^2 λ + 
                 3 λ (1 + λ)^2))/(1 + λ)^3 + \
((2 - r)/(1 + λ))^(-3 + 
              n) (-λ - ((-2 + r) (10 + 
                    2 (-4 + r) r + (-2 + 3 r) λ + (-4 + 
                    3 r) λ^2))/(1 + λ)^3)))/(r - 
          r ((2 - r)/(1 + λ))^
           n)) (2 + ((-2 + r)^4 (1 + λ)^
           n (-1 + r + λ) (8 + 
             2 (-3 + r) r + (-1 + 
                r (5 + (-3 + r) r)) λ + (-5 + 
                r^2) λ^2 + (-3 + 
                r) λ^3 + λ^4) + (2 - r)^

           n (1 + λ)^3 (4 r^5 λ + 
             r^4 (4 + (-27 + λ) λ) + 
             2 r^3 (-13 + λ (33 + λ + 
                   3 λ^2)) + 
             2 r^2 (32 + λ (-27 + λ (-9 + (-13 + \
λ) λ))) + (-1 + λ) (1 + λ) (-28 + \
λ (-37 + λ (-1 + λ + λ^2))) + 
             2 r (-1 + λ) (35 + λ (46 + λ (28 \
+ λ (2 + λ))))))/(2 (-2 + 
            r)^4 r (1 + λ)^3 ((2 - r)^n - (1 + λ)^
            n))))
f2[λ_, n_] := 
 f1[λ, n] /. r -> Sqrt[4 - (1 + λ)^2]

Plot3D[f2[λ, n], {λ, 0, 1}, {n, 7, 500}, 
 PlotPoints -> 50]

I'm trying the following, but the code is running for many hours, but with no solution or error, nothing:

True === FullSimplify[f2[λ, n] <= 0, 
  Assumptions -> 
   n ∈ Integers && n > 7 && λ ∈ Reals && 
    0 < λ <  1]

which may be indicative that I'm following the wrong route. So, I'd like to ask: what is the proper way to verify the inequality?

$\endgroup$
2
$\begingroup$
Clear["Global`*"]

f1 is

f1[λ_, 
   n_] := (1/
     64) (-64 - (8 λ (-4 + 2 r + λ + (-2 + r) r λ + 
          2 λ^2 + λ^3) ((-2 + r)^4 + (2 - r)^
            n (1 + λ)^(4 - n)) (5 + (-4 + 
             r) r + λ (2 + λ)))/((-2 + 
           r)^4 r (1 + λ)^3 (-1 + ((2 - r)/(1 + λ))^n)) + 
     64 (1 - ((-1 + λ)^2 (((2 - r)/(1 + λ))^
              n + (-2 + r)^2/(1 + λ)^2))/((-2 + 
             r) r (-1 + ((2 - r)/(1 + λ))^
              n))) (1 + ((-1 + λ) (1 + λ) (((2 - 
                  r)/(1 + λ))^
              n + (-2 + r)^2/(1 + λ)^2))/((-2 + 
             r) r (-1 + ((2 - r)/(1 + λ))^n))) + (4 (-1 + 
          r + λ) (-4 + 2 r + λ + (-2 + r) r λ + 
          2 λ^2 + λ^3) (1 + (-2 + 
              r)^2/(1 + λ)^2) (-(-2 + r)^(2 n) (1 + λ)^(8 - 
              2 n) (-20 + 
             2 r (13 + (-6 + r) r) + λ + (-2 + r) r λ + 
             2 λ^2 + λ^3) + (-2 + r)^7 (10 + 2 (-4 + r) r + 
             6 λ + r (5 + (-4 + r) r) λ + 
             2 (4 + r) λ^2 + (6 + r) λ^3 + 
             2 λ^4) + (2 - r)^(2 + n) (1 + λ)^(2 - 
              n) ((-2 + 
                r)^4 - (1 + λ)^4) (-(-4 + n) (-2 + 
                 r)^2 λ - (-4 + n) λ (1 + λ)^2 - 
             2 (-2 + r) (1 + λ) (-3 + n + λ))))/((2 - 
           r)^7 (1 + λ)^3 (3 - 
          r + λ) (r - r ((2 - r)/(1 + λ))^n)^2) + 
     4 (-4 λ + (2 (1 + λ) (2 + ((-2 + r) (-4 - 
                  2 r (-1 + λ) + r^2 λ + 
                  3 λ (1 + λ)^2))/(1 + λ)^3 + ((2 - 
                   r)/(1 + λ))^(-3 + 
                 n) (-λ - ((-2 + r) (10 + 
                    2 (-4 + r) r + (-2 + 3 r) λ + (-4 + 
                    3 r) λ^2))/(1 + λ)^3)))/(r - 
           r ((2 - r)/(1 + λ))^n)) (2 + ((-2 + r)^4 (1 + λ)^
             n (-1 + r + λ) (8 + 
              2 (-3 + r) r + (-1 + r (5 + (-3 + r) r)) λ + (-5 + 
                 r^2) λ^2 + (-3 + r) λ^3 + λ^4) + (2 -
                r)^n (1 + λ)^3 (4 r^5 λ + 
              r^4 (4 + (-27 + λ) λ) + 
              2 r^3 (-13 + λ (33 + λ + 3 λ^2)) + 
              2 r^2 (32 + λ (-27 + λ (-9 + (-13 + λ) \
λ))) + (-1 + λ) (1 + λ) (-28 + λ (-37 + \
λ (-1 + λ + λ^2))) + 
              2 r (-1 + λ) (35 + λ (46 + λ (28 + \
λ (2 + λ))))))/(2 (-2 + r)^4 r (1 + λ)^3 ((2 - r)^
              n - (1 + λ)^n))));

f2 is

f2[λ_, n_] := f1[λ, n] /. r -> Sqrt[4 - (1 + λ)^2]

λ must be less than 1 since

Limit[f2[λ, n], λ -> 1]

{* Indeterminate *)

You must restrict n to be positive since

Assuming[0 <= λ < 1, f2[λ, -1] > 0 // Simplify]

(* True *)

Then

dom = FunctionDomain[{f2[λ, n], 0 <= λ < 1, 
    n >= 0}, {λ, n}] // 
  FullSimplify[#, {0 <= λ < 1, n >= 0}] &

(* λ < 1 && 
 2 n ∈ Integers && (1 + λ)^
  n != (2 - Sqrt[-(-1 + λ) (3 + λ)])^n && 
 Sqrt[-(-1 + λ) (3 + λ)] (-1 + ((
      2 - Sqrt[-(-1 + λ) (3 + λ)])/(1 + λ))^n) != 0 *)

The function is only real when n is a half-integer or an integer, e.g.,

Cases[Table[{n, f2[1/2, n]} // N, {n, 7, 10, 0.01}], {_, _Real}]

(* {{7., -0.0198283}, {7.5, -0.0205678}, {8., -0.0211701}, {8.5, -0.0216021}, \
{9., -0.0219313}, {9.5, -0.0221699}, {10., -0.0223461}} *)

To find a counterexample, i.e., a case for positive value

(max = NMaximize[{f2[λ, 15/2], 0 <= λ < 1}, λ,
    WorkingPrecision -> 15]) // InputForm

(* {157.718867374661801065017629336351\
13483888`15., {λ -> 0.999999996825\
62313888743502729994361289`15.}} *)

The function will be positive for half-integer values of n and values of λ sufficiently close to 1

f2[1 - 10^-9, 35/2] // N[#, 20] &

(* 51.603721769605913357 *)
| improve this answer | |
$\endgroup$
  • $\begingroup$ Could you explain to me the appended part // FullSimplify[#, {0 <= λ < 1, n >= 0}] & $\endgroup$ – capadocia May 4 at 22:37
  • $\begingroup$ It determines the domain for which f2 is real. See FunctionDomain documentation. When you see a function that you don't understand, highlight it and press F1 for help. $\endgroup$ – Bob Hanlon May 4 at 22:43
  • $\begingroup$ I was referring to the appended portion only. When I ran your code, I got a different output on that line (incomplete in comparison to yours). $\endgroup$ – capadocia May 4 at 23:07
  • $\begingroup$ Postfix use of FullSimplify to simplify the output of FunctionDomain using the assumptions {0 <= λ < 1, n >= 0} $\endgroup$ – Bob Hanlon May 4 at 23:14

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.