Ordering preference for two zero mean Gaussian outcomes

Question

Let $X\sim \mathcal{N}(0,1)$ be a standard Gaussian random variable. If we let $f_a(x)\triangleq\mathbb{E}[\max\{aX,x\}]$ for $a,x >0$, how to prove that $$f_a(f_b(1))<f_b(f_a(1))~~\text{for }0<a<b.$$ Saying it differently, if $X'\sim X$ independently, how to show that you would prefer to first try $bX$, to then eventually try $aX'$, and eventually finish by taking $1$, rather than trying $aX'$ first, to then eventually try $bX$, to eventually finish by taking $1$.

Answer 1

It seems like it is high time to handle this one. The main difficulty here is that there seems to be no conceptual reason for the inequality to be true: it just comes up valid before one numerical constant exceeds another one, not because there is a natural class of functions that satisfy it. I'll use my standard bag of tricks though, in view of the recent discussion with mathworker21 in Is this function concave? (or, if you have followed some of my other posts, with Iosif Pinelis), I'll try to elaborate a bit on how I'm normally pulling such tricks through and what I think about why I'm more lucky with them than other people, so the discussion will be partially philosophical. If you are not interested in that part and my ridiculous opinions, just skip the corresponding passages and enjoy the mathematics in between them. I know that every time I want to talk to my friends about some things in serious, they claim that I show off and get epatant, so I more or less expect the same reaction from strangers too. Feel free to downvote :-)

Doron Zeilberger once said "Science is something that we understand well enough to explain it to a computer. Art is everything else we do." (see Foreword in his famous book A=B with Marko Petkovsek). I don't mind the idea per se, but I find it hopelessly incomplete as stated. The complement (IMHO) is (as far as mathematics is concerned) "Proof is something that can be verified by a human being without pen and paper. The rest is arcane magic." In other words, not only should humans be able to communicate to computers efficiently, but also computers should be able to convey their arguments to the humans. Of course, neither human, nor a computer is obliged to communicate the whole chain of thought, but both should be able to present something written in the language of the other party and verifiable by it within that other party abilities.

There are a few simple and (nearly) algorithmic techniques I want to discuss here. I'm a fairly bad writer, definitely no match to Polya, but, if you have some patience to bear with me, I hope at least some part of the message will get conveyed.

Let's start with two inequalities we will need for the current problem.

Inequality 1 $$ \log 2\le 0.7. $$ The proof is via the truncated Taylor series (a typical example of the main theme we are discussing: the infinite Taylor series is precise but impossible to compute while any truncation loses precision while can be obtained by finite number of additions and multiplications), of course, but which one? Definitely not for $\log(1+x)$ with $x=1$: that is not human computable. $\log(1-x)$ with $x=\frac 12$ seems better, but given that the accuracy is below $0.007$ and even $5\cdot 2^5$ is only $160$, it doesn't look attractive either. So, we, probably, want to exponentiate. Then we get $$ e^{0.7}>2\,. $$ Now $e^7>1; 1+0.7=1.7; 1+0.7+\frac 12 0.49=1.7+0.245=1.945$, so we lack just $0.055$ for the next term. It is $0.49\cdot 0.7/6=0.049+0.049/6>0.049+0.048/6=0.049+0.008=0.057$, which is good for us.

The whole computation can be verified in one's head. Note that I switched several times from what has been already gained to what is left to gain once I computed the "easy" pieces and simplified afterwards. That is a normal feature of the human bookkeeping: get what you can easily get and when comparing the remaining parts, make the inequality cruder but simpler. Dividing $49$ by $6$ in decimals would take forever, so we have to resort to truncation again and if so, why not to start with the natural truncation that produces the whole quotient? If it is insufficient look at what is left, add one digit a time, never rush to the entire series unless you can compute it and try to simplify the inequality if it doesn't look obvious yet. It may all sound idiotic now, but when we come to estimating some non-elementary integrals, the technique will be exactly the same, so I'm dwelling on it now on an example that can be explained to a 5-year old.

The next one is a bit harder but I'll go over it faster. Since you know what to look for now, it will be the same technique.

Inequality 2 $$ 3.14<\pi<3.2 $$ We shall use Machin's representation $\pi=16\arctan \frac 15-4\arctan \frac1{239}$. One can have an interesting discussion on how a CAS could come up with it and choose it among other possible representations, but let's skip it for now.

The upper bound is now immediate for human verification: $16\arctan \frac 15<\frac{16}5=3.2$. The point is to get the lower bound. We'll truncate the power series for $\arctan\frac 15$ to $\frac 15-\frac 1{3\cdot 5^3}$ and bound $\arctan\frac 1{239}$ by $\frac{4}{239}$. We thus need to check that $$ \frac{16}{3\cdot 5^3}+\frac 4{239}<0.06 $$ or $$ \frac{8}{3\cdot 5^3}+\frac 2{239}<0.03 $$

*First attempt at a human verifiable proof: (the model of a human I'm considering cannot multiply 2-digit numbers but knows some algebra (of the type $\frac 1n=\frac 1{n+1}+\frac 1{n(n+1)}$)

Note that $\frac{8}{375}=\frac 8{376}+\frac 8{375\cdot 376}= \frac 1{47}+\frac 8{375\cdot 376}<\frac 1{47}+0.0001$ ($300\times 300=90000$ already). Similarly, $\frac 2{239}=\frac{2}{240}+\frac 2{239\cdot 240}< \frac{2}{240}+\frac 2{239\cdot 240}$. Thus, we need to show that $$ \frac 1{47}+\frac 2{240}+0.0001+\frac 2{239\cdot 240}<0.03\,. $$ But $\frac 1{47}=\frac{1}{48}+\frac 1{47\cdot 48}<\frac{1}{48}+0.001$, $\frac 1{48}+\frac 2{240}=\frac 7{240}$, $\frac 7{240}+\frac 2{239\cdot 240}\le \frac 7{240}+\frac {7\cdot 2}{238\cdot 240}=\frac 7{238}=\frac 1{34}$, so we are left with $$ \frac 1{34}+0.0001<0.03\,, $$ or $\frac{3}{100}-\frac{1}{34}=\frac 2{3400}>\frac 2{20000}=0.0001$

Did you like that? Probably not, and neither did I. It is human verifiable, but it needs more than 4 short term memory registers. Not good. However this is typical of what first comes to your head when you try playing such games. Let's try again:

Second attempt at a human verifiable proof: $$ \frac{8}{3\cdot 5^3}+\frac 2{239}<0.03 $$ $$ \frac{8}{5^3}+\frac 6{239}<0.09 $$ $$ \frac{8\cdot 2^3}{10^3}+\frac 6{239}<0.09 $$ $$ 0.064+\frac 6{239}<0.09 $$ $$ \frac 6{239}<0.09-0.064=0.026 $$ $$ \frac 6{240}+\frac 6{240\cdot 239}=0.0025+\frac 6{240\cdot 239}<0.026 $$ $$ \frac 6{240\cdot 239}<\frac 6{40000}<\frac 6{6000}=0.001 $$

Much better, isn't it? One short term memory register used and all multiplications/divisions are trivial. That is the whole difference between a "cumbersome" approach and an "elegant" one and the formal score function is pretty clear. Can one do even better? Perhaps. Computers can consider thousands of possible derivation chains per second and I tried just 3 or 4 in half an hour before presenting these two here. So, it would be nice to teach machines (or, at least, students) some arithmetic like that before they start handling integral inequalities. "Arithmetic for analysis" might be quite a useful course, making much more sense IMHO than the widespread "Algebra for calculus".

I thanks everybody who had patience to read all this. I couldn't explain what I meant on anything simpler than inequalities for rational numbers with seemingly ugly denominators. Now we will play exactly the same game with (occasionally double) integrals and functional inequalities. I'll go faster from now on and spare you from seeing imperfect attempts (but they were there and related to the final argument as Attempt 1 to Attempt 2).

Convenient renormalization

Let $g(x)=E(\max X,x)$, $x>0$ where $X$ is a standard normal. The inequality we want can be rewritten as $$ ag(\tfrac{g(x)}{a})<g(ag(\tfrac{x}a) , x>0, 0<a<1\,. $$ Reduction to a functional inequality for a decaying convex function

Note that $g(x)=x+\varphi(x)$ where $$ \varphi(x)=\frac 1{\sqrt{2\pi}}\int_x^\infty (t-x)e^{-t^2/2}\,dt= e^{-x^2/2}\int_0^\infty e^{-tx}te^{-t^2/2}\,dt=\frac 1{\sqrt{2\pi}}e^{-x^2/2}\psi(x)\,. $$
We also have $$ \varphi'(x)=-\frac 1{\sqrt{2\pi}}\int_x^\infty e^{-t^2/2}\,dt= -e^{-x^2/2}\int_0^\infty e^{-tx}e^{-t^2/2}\,dt=-\frac 1{\sqrt{2\pi}}e^{-x^2/2}\psi_1(x)\,. $$
and $$ \varphi''(x)=\frac 1{\sqrt{2\pi}} e^{-x^2/2}\,. $$
So at the very least $\varphi$ is convex and decreasing. We will also need the relation $\varphi''(x)=\varphi(x)-x\varphi'(x)$ (you can get it either from the integral representations noticing that the sum on the right has an elementary antiderivative, or by taking the derivatives of both sides and the equation $\varphi'''(x)=-x\varphi''(x)$ together with the remark that everything decays fast near $+\infty$).

Why am I doing this decomposition? The underlying principle is very simple: extract the easy "large" part and work with the remaining small one. Now, once we take the $x+$ part out of $g$ and cancel everything that can be cancelled, our inequality becomes $$ \varphi(x)+a\varphi(\tfrac xa+\tfrac{\varphi(x)}a)<a\varphi(\tfrac xa)+\varphi(x+a\varphi(\tfrac xa))\,. $$ This doesn't look terribly exciting: too many $a$'s, but it is clear that $y=\frac xa>x$ plays some prominent role here, so let us rewrite it as $$ \varphi(x)+a\varphi(y+\tfrac{\varphi(x)}a)<a\varphi(y)+\varphi(x+a\varphi(y))\,, 0<a<1, x<y. $$ We generalized a bit here allowing $y$ and $x$ to be unrelated except for the trivial inequality between them. Now we have $3$ variables (obvious loss in the score function) but fewer occurrences of $a$ (obvious gain). For $a=1$, we get a rather elegantly looking inequality $$ \varphi(x)+\varphi(y+\varphi(x))\le \varphi(y)+\varphi(x+\varphi(y)\,, $$ which, taking into account that $\varphi$ is typically small, is very tempting to rewrite as $$ \varphi(x)-\varphi(x_\varphi(y)\le \varphi(y)-\varphi(y+\varphi(x))\,. $$ That partial case would be an obvious gain in the simplicity score, so it is tempting to try to get rid of $a$ reducing to this case.

Getting rid of $a$.

Take $z>y$ such that $\varphi(z)=a\varphi(y)$. Then the inequality will become $$ \varphi(x)+a\varphi(y+\tfrac{\varphi(x)}a)<\varphi(z)+\varphi(x+\varphi(z))\, 0<a<1, x<y, \varphi(z)=a\varphi(y)\,, $$ so it will be suffice to check that $$ a\varphi(y+\tfrac{\varphi(x)}a)<\varphi(z+\varphi(x)) $$ or, plugging $a=\frac{\varphi(z)}{\varphi(y)}$ in, $$ \frac{\varphi(z)}{\varphi(y)}\varphi(y+\varphi(x)\tfrac{\varphi(y)}{\varphi(z)})<\varphi(z+\varphi(x))\,. $$ Obviously, $\varphi(x)>0$ now becomes free parameter, so let us call it $T$ (small but tangible gain in the simplicity score a machine can easily detect). Also let us bring $z$'s to one side and $y$'s to the other as much as we can (another purely mechanical move). We'll get $$ \frac{\varphi(y+\tfrac{\varphi(y)}{\varphi(z)}T)}{\varphi(y)}< \frac{\varphi(z+T)}{\varphi(z)}\,. $$ Now let us use one more standard technique: elimination of trivial cases for the gain of extra assumptions.

Since $\varphi(y)>\varphi(z)$, if $y+\tfrac{\varphi(y)}{\varphi(z)}T>z+T$, there is nothing to prove. Thus we may assume the contrary. Then $y+\tfrac{\varphi(y)}{\varphi(z)}t<z+t$ for $0<t<T$ and subtracting $1$ from both sides, we can write the inequality in the "incremental" form: $$ \frac{\varphi(y+\tfrac{\varphi(z)}{\varphi(y)}T)-\varphi(y)}{\varphi(y)}< \frac{\varphi(z+T)-\varphi(z)}{\varphi(z)}\,, $$ which cries for the integral representation with $\int_0^T\frac d{dt}\dots\,dt$, resulting in $$ \int_0^T\varphi'(y+\tfrac{\varphi(z)}{\varphi(y)}t)\,dt<\int_0^T\varphi'(z+t)\,dt\,. $$ But $\varphi'$ is increasing (convexity) and now, due to our additional assumption we gained by eliminating the trivial case, we heve the pointwise inequality between integrands all the way from $0$ to $T$. Done.

This part was easy because the corresponding inequality is "conceptual": it holds for the entire class of the decreasing convex functions. All this was done by just slowly lowering the complexityity score and looking 2 moves ahead at most. The AI has a huge advantage here because it can quickly check if the generalization seems correct by brute force computations. I had to rely on more sophisticated heuristic techniques to figure out what is believable and what is not to avoid any too bold moves.

Anyway, we now got rid of $a$ entirely and have a nicely looking inequality $$ \varphi(x)-\varphi(x+\varphi(z))\le \varphi(z)-\varphi(z+\varphi(x)), 0<x<z\,. $$

Now I'll use my usual hammer, which is an analogue of the algebraic statement that $\frac {x}{x+1}$ is increasing for $x>0$ (not because one can take the derivative using the quotient rule, but because $\frac {x}{x+1}=\frac 1{1+\frac 1x}$ and $x\mapsto \frac 1x$ is obviously decreasing, of course).

Elementary lemma (see the post mentioned in the beginning for the proof).

If $\mu$ is a positive measure on $(0,+\infty)$ and $f$ is a decreasing (increasing) function, then $$ x\mapsto \frac{\int_0^\infty f(t)e^{-xt}\,d\mu(t)}{\int_0^\infty e^{-xt}\,d\mu(t)} $$ is increasing(decreasing) in $x>0$.

Is it possible to teach a machine to recognize symbolic instances of such principle (and a few others)? I see no reason why not. The necessary and sufficient condition on the family $e^{-xt}$ for this principle to hold is easy to formulate and the recognition of common factor depending on $x$ and carrying it out is a child game for the modern CAS. For a human it is the already discussed on MO principle that "every mathematician has just a few tricks" (but can learn new ones!) so one can start with a CAS that has a few tricks too (even to implement human verifiable rational arithmetic would be a step forward from what outputs we typically get from our machine partners now).

We will use this lemma to show that $\frac{|\varphi'|}{\varphi}=\frac{\psi_1}{\psi}$ is increasing (immediate) and convex (will be done in the next section). Also we trivially have that $\frac{\varphi''}{|\varphi'|}=\frac 1{\psi_1}$ is increasing.

Convexity of $\frac{\psi_1}{\psi}$ We have $$ \left(\frac{\psi_1}{\psi}\right)'=\frac{\psi_1'\psi-\psi_1\psi'}{\psi^2} \\ = \frac 12\frac{\iint(t-s)^2e^{-x(t+s)}e^{-(s^2+t^2)/2}\,dt\,ds} {\iint tse^{-x(t+s)}e^{-(s^2+t^2)/2}\,dt\,ds} $$ (I symmetrized the numerator integral, of course; all double integrals are over $(0,+\infty)^2$ unless specified otherwise).

Switching to variables $\sigma=s+t$ and $\gamma=s-t$ and using symmetry, we can rewrite this ratio (up to a positive constant factor) as $$ \frac{\iint_{0<\gamma<\sigma}\gamma^2e^{-x\sigma}e^{-(\sigma^2+\gamma^2)/4}\,d\gamma\,d\sigma} {\iint_{0<\gamma<\sigma}(\sigma^2-\gamma^2)e^{-x\sigma}e^{-(\sigma^2+\gamma^2)/4}\,d\gamma\,d\sigma}\,. $$ For fixed $\sigma$ it makes sense to integrate over $\gamma$ using the change of variable $\gamma=\tau\sigma$, $0<\tau<1$, to get the ratio as $$ \frac{\int_0^\infty F(\sigma)e^{-x\sigma}e^{-\sigma^2/4}\,d\sigma} {\int_0^\infty G(\sigma)e^{-x\sigma}e^{-\sigma^2/4}}\,. $$ where $$ F(\sigma)=\sigma^3\int_0^1 \tau^2e^{-\tau^2\sigma^2/4}\,d\tau $$ and $$ G(\sigma)=\sigma^3\int_0^1(1-\tau^2)e^{-\tau^2\sigma^2/4}\,d\tau $$,. By our Lemma, to show that the initial ratio of integrals is increasing in $x$, it is enough to show that $\frac{F}{G}$ is decreasing in $\sigma$, which, by the lemma again (just use $\tau^2$ as a new variable and $\sigma^2$ as a new parameter) follows from the fact that $\frac{\tau^2}{1-\tau^2}$ is increasing in $\tau$.

Is there a reason beyond this? For a CAS it is enough to implement the principle "check all standard properties of the function and simple combinations of its derivatives you can". The calculus students are taught the lists of those standard properties and their verification techniques all the time with some partial success. Computers, which have perfect memory and no need to spend most of their time making a living, can learn them much faster if somebody bothers to teach them, of course.

For a human a reason for choosing just these properties will be clear from what goes next.

We also have $\psi(0)=1, \psi_1(0)=\sqrt{\pi/2}$. The first one is an elementary integral; the second one is well-known to humans and machines alike.

Now again, let us eliminate the trivial case. Note that $$ \varphi(x)-\varphi(x+\varphi(z))\le |\varphi'(x)|\varphi(z) $$ and $$ \varphi(z)-\varphi(z+\varphi(x))\ge \varphi(z)(1-e^{-Z\varphi(x)}), Z=\frac{|\varphi'(z)|}{\varphi(z)}\,. $$ Thus, if $Z\varphi(x)>\log\frac{1}{1-|\varphi'(x)|}$, the inequality holds. Since $|\varphi'(x)|$ is $\frac 12$ at $0$ and decreasing, we are fine every time $Z\varphi(x)>\frac 75|\varphi'(x)|$ (Inequality 1).

Now it is time for Taylor expansions. We'll use the integral form of the remainder. It is something we teach our analysis students to do every time they see the difference with presumably small increment. $$ \varphi(x)-\varphi(x+\varphi(z))=-\varphi'(x)\varphi(z)-\varphi(z)^2\int_0^1(1-t)\varphi''(x+t\varphi(z))\,dt \\ = -\varphi'(x)\varphi(z)-\varphi(z)^2\varphi''(x)\int_0^1(1-t)e^{-x\varphi(z)t-[t\varphi(z)]^2/2}\,dt $$

Doing the same representation for $\varphi(z)-\varphi(z+\varphi(x))$ and dividing both parts by $\varphi(x)\varphi(z)$, we get the inequality $$ \frac{|\varphi'(z)|}{\varphi(z)}- \frac{|\varphi'(x)|}{\varphi(x)}\ge \frac{\varphi''(z)}{\varphi(z)}\varphi(x) \int_0^1(1-t)e^{-z\varphi(x)t-[t\varphi(x)]^2/2}\,dt- \frac{\varphi''(x)}{\varphi(x)}\varphi(z) \int_0^1(1-t)e^{-x\varphi(z)t-[t\varphi(z)]^2/2}\,dt\,. $$ Note now that $\varphi(x)>\varphi(z)$ and $z\varphi(x)>x\varphi(z)$, so we can replace the integral in the subtrahend by the (smaller) one in the minuend and thus strengthen the inequality simultaneously simplifying it. After we make the integrals common, we raise them to $$ I=\int_0^1(1-t)e^{-z\varphi(x)t}\,dt $$ just dropping the $[t\varphi(x)]^2/2$ part. Of course, the natural move would be to drop the $e^{-z\varphi(x)t}$ as well and come up with a clean neat $\frac 12$. This is exactly what I did initially, but that turned out to be going too far in the simplification game, so I had to step back and keep the integral as written for the moment. It is not that I drop and keep the terms for no apparent reason: I drop all I can drop at the first attempt and then reintroduce the dropped terms one by one starting with most "heavy" ones until I make the ends meet. Let's think of that symbol $I$ as "improvable $\frac 12$" for now. Denoting $X=\frac{|\varphi'(x)|}{\varphi(x)}$, $Z=\frac{|\varphi'(z)|}{\varphi(z)}$ and recalling the identity $\varphi''(x)=\varphi(x)+x|\varphi'(x)|$, so $\frac{\varphi''(x)}{\varphi(x)}=1+xX$, we can write the resulting inequality as $$ Z-X\ge I[(zZ+1)\varphi(x)-(xX+1)\varphi(z)]=I[(zZ-xX)\varphi(x)]+(xX+1)(\varphi(x)-\varphi(z))] \\ =I z\varphi(x)(Z-x)+I[(z-x)X\varphi(x)+(xX+1))(\varphi(x)-\varphi(z))] \,. $$
Now recall that $X\varphi(x)=|\varphi'(x)|$ and $xX+1=\frac{\varphi''(x)}{\varphi(x)}$. Also move the first term to the left, replace $I$ on the LHS by \frac 12 (but not on the RHS) and estimate $\varphi(x)-\varphi(z)\le|\varphi'(x)|(z-x)$.
You'll get $$ (Z-X)(1-\tfrac 12z\varphi(x))\ge I(z-x)|\varphi'(x)|(1+\tfrac{\varphi''(x)}{\varphi'(x)}) $$ to prove. Why this form and not another? You have finite choice here with the general guidance that factorization is good. Of course, I initially kept it in just some equivalent form with the options to replace some expressions by identically equal ones. It took a couple of hours to finalize on this particular one but it was just routine trial and error, nothing ingenious.

Recall now that $x\mapsto \frac{|\varphi'(x)|}{\varphi(x)}=\frac{\psi_1(x)}{\psi(x)}$ is increasing convex. At $x=0$ its derivative is $\frac{\pi}2-1$. At $+\infty$ you can easily check by, say, Laplace asymptotic formula (though more elementary ways are also available) that $\psi_1(x)\sim 1/x$ and $\psi(x)\sim 1/x^2$ at $+\infty$, so the ratio is asymptotic to $x$, which for a convex increasing function is possible only if its derivative is asymptotic to $1$. Thus $$ \frac\pi 2-1\le \left(\frac{|\varphi'(x)}{\varphi(x)|}\right)'\le 1. $$ Why? Again the same principle: if you don't know what to do next, figure out a few things that look useful. Why is that one useful? For a human it is obvious: the difference ratio $\frac{Z-X}{z-x}$ cries for the MVT so loudly that you can hear that cry near Jupiter, if not Betelgeuse. And that requires the bounds for the derivative we have just done.

Now, plugging the lower bound for the derivative on the LHS (and using the MVT, of course), we reduce the task to proving that $$ (\tfrac \pi 2-1)(1-\tfrac 12 z\varphi(x))\ge I|\varphi'(x)|(1+\tfrac{\varphi''(x)}{\varphi(x)}) $$ We want now to investigate the product of the last two factors on the RHS. It is a function of $x$ that rather obviously quickly decays at $\infty$. So, faithful to our principle "Investigate all functions you meet for standard properties" let's see if it is decreasing all the way through. Taking its derivative, we get $$ -\varphi''(x)+\varphi'''(x)\tfrac{|\varphi'(x)|}{\varphi(x)}+\varphi''(x)(\tfrac{|\varphi'(x)|}{\varphi(x)})'. $$ But $\varphi'''(x)<0$ and $(\tfrac{|\varphi'(x)|}{\varphi(x)})'\le 1$ as we figured out short time ago. So yeah, it is decreasing. The value at $0$ is $\frac 12(1+1)=1$, so we can just drop this factor altogether. We are now left with $$ (\tfrac \pi 2-1)(1-\tfrac 12 z\varphi(x))\ge I $$ Clearly, at $z=0$ we have the LHS equal to $\tfrac \pi 2-1>0.57$ (Inequality 2). Thus if the inequality fails, $z\varphi(x)$ should be not too small, which means that $Z\varphi(x)$ should be even larger and we can hope that it will then beat $\frac 75|\varphi'(x)|$ throwing us into the domain when the inequality is trivial. Let's try to implement that strategy (it is not guaranteed to succeed and it actually won't if we just replace $I$ by $\frac 12$ on the RHS but, fortunately, keeping $z\varphi(x)$ in $I$ helps a lot and, even more fortunately, we have exactly the same $z\varphi(x)$ on the LHS). Let's denote it by $\rho$. In the bad case we have $$ 0.57(1-\tfrac\rho 2)<\int_0^1(1-t)e^{-\rho t}\,dt\,. $$ Tayloring the RHS to the quadratic terms, which is a clear overestimate (it should be obvious at least for $\rho<1$, which is enough for our purposes and is machine detectable), we get $$ RHS\le \frac 12-\frac\rho 6+\frac{\rho^2}{24}. $$ Now the rate at which the RHS decays is at most $\frac 16$ while the rate at the LHS is $>\frac 14$, so the curves cross just once. We will show that the crossing point is beyond $\rho=\frac 12$.

Why? Here the AI shines: it can easily find the root of the quadratic equation (or even the original transceendental one) with high precision. However, IMHO, it should keep that root to itself and present a human verifiable fraction instead. Finding that fraction is not hard either. I don't think anybody will argue that it is difficult to program. However, it has never been programmed and we still get human unverifiable statements like $\rho>0.12345678910$ from our computers when we ask them to prove our numeric inequalities. They can just well output "(out 15) true" and some people start believing that it is all we can possibly hope for. I don't think so.

Thus we need to check that $0.57(1-\frac 14)>\frac 12-\frac{1}{6\cdot 2}+\frac 1{24\cdot 2^2}$. Multiplying by $24\cdot 2^2$, we get $$ 0.57\cdot 3\cdot 24> 48-8+1\,, $$ i.e. $$ 1.14\cdot 36>41 $$ $$ 0.14\cdot 36=3.6+1.44=5.04>5 $$ finishing the proof.

Thus $\rho>\frac 12$. Since $\rho=z\varphi(x)$, we have $$ Z\varphi(x)\ge \sqrt{\tfrac \pi 2}\varphi(x)+0.57z\varphi(x)\ge \sqrt{\tfrac \pi 2}\varphi(x)+0.285 $$ (I estimated $Z$ by its value at zero plus the minimum of the derivative times $z$) This has to beat $\frac 75|\varphi'(x)|$. Thus we need to show that $$ \max_{x>0}(\tfrac 75|\varphi'(x)|-\sqrt{\tfrac \pi 2}\varphi(x))=\frac 75\max_{x>0}(|\varphi'(x)|-\tfrac 57\sqrt{\tfrac \pi 2}\varphi(x))\le 0.285\,. $$ Now, $\frac 57\sqrt{\tfrac \pi 2}>\sqrt{\frac 2\pi}$ (this is equivalent to $\frac\pi 2>\frac 75$, i.e., $\pi>\frac{14}{5}=2.8$), so it is enough to show that $$ \frac 75\max_{x>0}(|\varphi'(x)|-\sqrt{\tfrac 2 \pi}\varphi(x))\le 0.285\,. $$ However the function under the maximum sign now has $0$ derivative at $0$ and, since $\frac{\varphi''(x)}{|\varphi'(x)|}$ is increasing, negative derivative for all $x>0$. Thus this maximum is at $x=0$ where the value of the LHS is $\frac 75(\frac 12-\frac 1\pi)<\frac 75(\frac 12-\frac 1{3.2})$. Thus we are left with $$ \frac 75\left(\frac 12-\frac{10}{32}\right)=\frac 75\frac{6}{32}=\frac{42}{160} \\ =\frac{40}{160}+\frac 2{160}<0.25+0.02=0.27<0.285. $$ The end.

So now I showed the complete game. It is akin to chess: at each step you have finitely many moves and just try to simplify, simplify, and simplify with the score function that I tried to present and even occasionally formalize. Like in the chess I do not see the final winning position until I nearly arrive there; I just try to improve the current one a little bit. If you want to understand why I made each move the way I did, just ask yourself what moves you would consider instead. It is not a rhetorical question: each position I passed through had several legitimate moves. I didn't show them except on the simple rational arithmetic example because this post is already too long to the extent of possibly being "inappropriate for MO", but if you want to really understand the strategy, you should find those alternative moves yourself in this particular game, see what positions they lead to, and compare the resulting positions to my resulting positions and the positions before the move. Then, if you feel like the move is disadvantageous even compared to the original position (or advantageous even compared to mine), try to discern the criteria you are using for such evaluation and formalize them. Mine are embarrasingly simple: the total formula length, the number of different symbols, the number of occurrences of each symbol, the possibility to factor, etc. Most of the time I sacrifice precision, i.e., make the inequality stronger or more general, but if I can gain simplification with an identity, I certainly play it first. This particular game took 7 evenings (mainly due to considering the alternative moves that led nowhere). An intelligent AI would spend a few milliseconds on it. How much you spend on its full analysis depends on your basic skills. But I want to emphasize that there is nothing "amazing" in it and if you find the argument reasonably elegant, I showed where this elegance comes from by comparing Attempt 1 and Attempt 2 for rational arithmetic problem. The remarks of the kind "I have absolutely no idea how you came up with this!" please my ego of course, but also give me deep frustration because they mean that I failed to communicate the underlying ideas entirely and that instead of enabling the reader to prove his next elementary inequality by himself, I just pulled out one more rabbit from the hat. This game is really simple enough to learn and even to "communicate to computers". The price of this communication is as usual: time and effort. The ultimate gain is machines that can produce easily verifiable arguments instead of thousands of megabytes of incomprehensible gibberish that are currently called "computer assisted proofs". Not every such game will be winnable, of course. But not every true statement can be proved either. Whether the gain is worth the price is for everyone to decide by yourself. The life is short and everybody has his or her only priorities. I just tried to convince you that this game is close enough to chess to use the same general techniques in programming. Of course, if you understand and can play it better than I, I will be happy to hear your opinions about it. Your techniques may easily be superior to mine. Just show them on an example of a real proof construction for an unknown problem like I did and we'll compare both the results and the techniques.

At last one may ask whether one should learn to play such games at the expense of the time he could do "serious research" instead. I don't think there is anything "serious" enough in this life to justify the total abandonment of the pleasure of playing but if you prefer to be a "mathematical samurai" I see no problem with that either. I'll leave it to other people to judge how much (or whether) I'm capable of the so called "serious research". I just want to say that for me the only two tangible distinctions between different mathematical problems are whether I can understand their statements or not and whether I can solve them or not and that I employ in "serious research" pretty much the same techniques like father Brown from Chesterton novels used exactly the same method to catch thieves and to talk to angels. I just cannot explain them on examples of that level. I honestly tried. The message did not go through. Let's see if it will at the level of elementary arithmetic and functional inequalities for explicit functions.

Thanks to all who had patience to read up to this point!