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$
0

1 Answer 1

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 *)
$\endgroup$
4
  • $\begingroup$ Could you explain to me the appended part // FullSimplify[#, {0 <= λ < 1, n >= 0}] & $\endgroup$
    – Ararat
    May 4, 2020 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, 2020 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$
    – Ararat
    May 4, 2020 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, 2020 at 23:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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