# How to verify an inequality?

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?

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\
1348388815., {λ -> 0.999999996825\
6231388874350272999436128915.}} *)


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 *)

• Could you explain to me the appended part // FullSimplify[#, {0 <= λ < 1, n >= 0}] & May 4, 2020 at 22:37
• 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. May 4, 2020 at 22:43
• 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). May 4, 2020 at 23:07
• Postfix use of FullSimplify to simplify the output of FunctionDomain using the assumptions {0 <= λ < 1, n >= 0}` May 4, 2020 at 23:14