How to prove or disprove an inequality with Mathematica?

I mean there exist $$\lambda>0, x\in \mathbb R$$ s.t. the inequality $$\frac{3^{\lambda } e^x+e^{3 x}+1}{2^{\lambda } e^{2 x}}<\frac{1}{10^{100}}$$ is valid.

Here are my unsuccessful attempts.

Resolve[Exists[\[Lambda], \[Lambda] > 0, Exists[x, (1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) <
10^-100]], Reals]


returns the input. The same issue with

Minimize[{(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x), \[Lambda] > 0}, {\[Lambda], x}]


and

FindInstance[(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) <
1/10^100 && \[Lambda] > 0, {\[Lambda], x}, Reals]


The result of the command

NMinimize[{(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x), \[Lambda] > 0}, {\[Lambda], x}]


{0., {\[Lambda] -> 425.496, x -> 236.227}}

is not any proof because 0. may be greater than 0.

• The command MinLimit[(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/ E^(2 x), {\[Lambda], x} -> {Infinity, Infinity}, Direction -> "FromBelow"] results in -Infinity which is wrong since the function takes only positive values. Mar 3, 2022 at 6:55

It is easier to solve equations and impose conditions on parameters (here fval ), than to solve inequations.

(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) <
10^-100 /. \[Lambda] -> 1800 /. x -> Log[10^420]

(*   True   *)


f = (1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x);


Get rid of the Exp

sol1 = Flatten@Solve[E^x == ex, x,Reals] // Quiet


Transform f < 10^-100 to f == fval with fval < 10^-100

f2 = f - fval /. sol1 // Together // Numerator


Get solutions for ex (=E^x) with conditions for fval and lambda

sol = Solve[f2 == 0 && ex > 0 && \[Lambda] > 0 && fval < 10^-100, ex,
Reals, Method -> Reduce];

sol // N

(*   {{ex -> ConditionalExpression[
Root[1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 2],
Root[-27 - 4 3^(3 \[Lambda]) -
2^(1 + \[Lambda]) 3^(2 + \[Lambda]) #1 +
6^(2 \[Lambda]) #1^2 + 2^(2 + 3 \[Lambda]) #1^3 &, 3] <
fval < 1.*10^-100
&& \[Lambda] > 1605.6]},

{ex ->
ConditionalExpression[
Root[1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 3],
Root[-27 - 4 3^(3 \[Lambda]) -
2^(1 + \[Lambda]) 3^(2 + \[Lambda]) #1 +
6^(2 \[Lambda]) #1^2 + 2^(2 + 3 \[Lambda]) #1^3 &, 3] <
fval < 1.*10^-100
&& \[Lambda] > 1605.6]}}   *)


{{ex -> ConditionalExpression[ Root[1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 2], Root[-27 - 4 3^(3 \[Lambda]) - 2^(1 + \[Lambda]) 3^(2 + \[Lambda]) #1 + 6^(2 \[Lambda]) #1^2 + 2^(2 + 3 \[Lambda]) #1^3 &, 3] < fval < 1.*10^-100 && \[Lambda] > 1605.6]}, {ex -> ConditionalExpression[ Root[1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 3], Root[-27 - 4 3^(3 \[Lambda]) - 2^(1 + \[Lambda]) 3^(2 + \[Lambda]) #1 + 6^(2 \[Lambda]) #1^2 + 2^(2 + 3 \[Lambda]) #1^3 &, 3] < fval < 1.*10^-100 && \[Lambda] > 1605.6]}}

Retransform x==Log[ex]

(Log[ex] /. sol) /. \[Lambda] -> 2500 /. fval -> 6/10 10^-100 //
N[#, 10] &

(*   {1244.432105, 1502.098616}   *)

Reduce[f2 == 0 && ex > 0 && \[Lambda] > 0 && fval < 10^-100, ex,         Reals]//N


\[Lambda] > 1605.6 && ((fval == Root[-27 - 4 3^(3 \[Lambda]) - 2^(1 + \[Lambda]) 3^(2 + \[Lambda]) #1 + 6^(2 \[Lambda]) #1^2 + 2^(2 + 3 \[Lambda]) #1^3 &, 3] && ex == Root[1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 2]) || (Root[-27 - 4 3^(3 \[Lambda]) - 2^(1 + \[Lambda]) 3^(2 + \[Lambda]) #1 + 6^(2 \[Lambda]) #1^2 + 2^(2 + 3 \[Lambda]) #1^3 &, 3] < fval < 1.*10^-100 && (ex == Root[1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 2] || ex == Root[ 1 + 3^\[Lambda] #1 - 2^\[Lambda] fval #1^2 + #1^3 &, 3])))

Edit made by @user6494. For the user's convenience (In order not to read the below comments.), I fixed the omitted Reals in  sol1 = Flatten@Solve[E^x == ex, x,Reals] // Quiet.

In version my version 8.0 Reals is not neccessary. (Akku14)

• Thank you. I will be waiting for a systematic solution produced by Mathematica. Mar 3, 2022 at 10:21
• Ehank you for your edit. 1. Unfortunately, your code is not commented. 2. sol = Solve[f2 == 0 && ex > 0 && \[Lambda] > 0 && fval < 10^-100, ex, Reals, Method -> Reduce] returns the input Mar 3, 2022 at 11:30
• Solve[ConditionalExpression[-(( 2^-\[Lambda] E^(-4 I \[Pi] ConditionalExpression[ 1, \[Placeholder]]) (-1 - 3^\[Lambda] E^( 2 I \[Pi] ConditionalExpression[1, \[Placeholder]]) ex - E^(6 I \[Pi] ConditionalExpression[1, \[Placeholder]]) ex^3 + 2^\[Lambda] E^( 4 I \[Pi] ConditionalExpression[1, \[Placeholder]]) ex^2 fval))/ex^2) == 0 && ex > 0 && \[Lambda] > 0 && fval < 1/ 100000000000.... 000000000000000000000000000000000000, ConditionalExpression[1, \[Placeholder]] \[Element] Integers] for me. Mar 3, 2022 at 11:30
• Works fine in version 8.0 Mar 3, 2022 at 11:32
• Akku14 (@ does not work.): Can you present the executed *.nb file and/or its PDF export through Dropbox? Mar 3, 2022 at 11:35

RegionPlot shows the possible solution space.

Assuming ((1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x))>0 (shown by OP):

eps = 10 ^-100;
gr=RegionPlot[Log[((1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x))] <
Log[eps], {\[Lambda], 0, 2500}, { x, 0, 2500 } ,
PlotPoints -> 500, FrameLabel -> {"\[Lambda]", " x "},MaxRecursion -> 5] // Quiet


gr[[1,1]][[1]] (*{{1613.23, 886.774}, {1618.24, 886.774}, {1623.25, 891.784},...}*) gives a lengthy list of solutionpoints.

• Thank you. Can you extract and indicate some values of \[Lambda] and x validating the inequality from the above plot? It works without Quiet for me in 13 on Windows 10. Mar 3, 2022 at 10:58
• Thank you for your edit. 1. Can you comment your gr[[1,1]][[1]] to be understandable for an average user? 2. Executing (1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) < 10^-100 /. {\[Lambda] -> 1613.2264514500012, x -> 886.7735485500076}, I obtain a warning "General::munfl: Exp[-1773.55] is too small to represent as a normalized machine number; precision may be lost. ", not only True, so this True is doubtful. Mar 3, 2022 at 11:38
• gr[[1,1]][[1]]  gives the list of points used in the GraphiComplex gr. Have a look inside gr witth ??gr . The condition includes numbers O[10^-100] , you should adapt Workingprecision to get trusting "True". Mar 3, 2022 at 11:38
• I don't think that I have to lead you through documentation! Lookup info GraphicsComplex as proposed by me some comments ago. Mar 3, 2022 at 12:47

Here is my tricky answer. First, the result of

Limit[(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) /.
x -> Log[3]/2*\[Lambda], \[Lambda] -> Infinity]


0

guarantees the existence of the required solution. Second,

NSolve[Expand[(1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) /.
x -> Log[3]/2*\[Lambda]] == 1/2*10^-100 && \[Lambda] >= 0 && \[Lambda] <= 3000 , \[Lambda]]


{{\[Lambda] -> 1610.42}}

finds a one solution of the inequality under consideration.

Addition. A simple approach which uses NMinimize is as follows.

NMinimize[{1, (1 + 3^\[Lambda]*E^x + E^(3 x))/2^\[Lambda]/E^(2 x) <
10^-100 && x^2 + \[Lambda]^2 >= 2*10^6 &&
x^2 + \[Lambda]^2 <= 10^7}, {x, \[Lambda]},
WorkingPrecision -> 100, Method -> "DifferentialEvolution"]


{1.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000,{x->1792.682158676924591695765318215658904932218868106718701333477115390170263646455485621517086104184032,\[Lambda]->2605.050993351464904744268828659450449353575490756371168671954922778805769014234476770620073231372436}}

• One may take a somewhat greater or smaller number than Log[3]/2. Mar 3, 2022 at 14:06