Suppose $y$ is defined by the following implicit equation: $ye^{-{xe^{y-2x}}} = 2xe^{-x},$ where $x,y\geq 0.$
I want to show that $y$ decreases as $x$ increases, when $x>\frac{1}{\sqrt{2}}$ and $y<\sqrt{2}$. Here is my work:
Suppose by contradiction that there exist some $x_1, x_2> \frac{1}{\sqrt{2}}$ such that $x_1<x_2 \implies y_1<y_2.$
From the above relation, we have
$$2x_1 = y_1e^{x_1(1-e^{y_1-2x_1})} \tag{1}$$
and
$$2x_2 = y_2e^{x_2(1-e^{y_2-2x_2})} .\tag{2}$$
Subtracting this results in the following:
$$2(x_2-x_1) = y_2e^{x_2(1-e^{y_2-2x_2})}- y_1e^{x_1(1-e^{y_1-2x_1})}.$$
From here, I am not sure how to proceed. The goal is to arrive at the contradiction $y_1>y_2$ with the assumption but getting this inequality seems somewhat challenging.
Following @jean's comment:
Take the natural logarithm on both sides of $(1)$ and $(2)$, and subtract:
\begin{align*}\ln{x_2}-\ln{x_1} &= \ln{y_2}-\ln{y_1} + x_2(1-e^{y_2-2x_2})- x_1(1-e^{y_1-2x_1})\\
& = \ln{y_2}-\ln{y_1} + (x_2-x_1) + (e^{y_1-2x_1}-e^{y_2-2x_2}).
\end{align*}
This looks much better compared to the exponential expression.
Best Answer
Some thoughts.
Fact 1. $1 - xy\mathrm{e}^{y - 2x} > 0$ on $(\frac{1}{\sqrt{2}}, \infty)\times (0, \sqrt{2})$.
Fact 2. For each fixed $x > \frac{1}{\sqrt{2}}$, the equation $ \ln y - x \mathrm{e}^{y-2x} = \ln 2 + \ln x - x$ has exactly one real solution $y \in (0, \sqrt{2})$.
$\phantom{2}$
Now, let $$F(x, y) := \ln y - x \mathrm{e}^{y-2x} - (\ln 2 + \ln x - x).$$ Clearly, $F(x, y)$ is continuously differentiable on $(\frac{1}{\sqrt{2}}, \infty)\times (0, \sqrt{2})$. By Fact 1, we have $$\frac{\partial F}{\partial y} = \frac{1}{y}\left(1 - xy\mathrm{e}^{y - 2x}\right) > 0.$$ By the Implicit Function Theorem, using Fact 2, the equation $F(x, y) = 0$ implicitly determines $y$ as a differentiable function of $x$, given that $x\in (\frac{1}{\sqrt{2}}, \infty)$.
Taking derivative with respect to $x$ on $\ln y - x \mathrm{e}^{y-2x} - (\ln 2 + \ln x - x) = 0$, we have $$\frac{1}{y} \cdot y'(x) - \mathrm{e}^{y-2x} - x \mathrm{e}^{y-2x}(y'(x) - 2) - \frac{1}{x} + 1 = 0$$ or $$\frac{1}{y}\left(1 - xy\mathrm{e}^{y - 2x}\right)y'(x) = \frac{1}{x} + (1 - 2x)\mathrm{e}^{y - 2x} - 1. \tag{1}$$
From (1), using Fact 1, it suffices to prove that $$\frac{1}{x} + (1 - 2x)\mathrm{e}^{y - 2x} - 1 < 0,$$ or $$\mathrm{e}^{y - 2x} > \frac{1/x - 1}{2x - 1}\tag{2}$$ given that $(x, y) \in (\frac{1}{\sqrt{2}}, \infty)\times (0, \sqrt{2})$ with $\ln y - x \mathrm{e}^{y-2x} = (\ln 2 + \ln x - x)$.
Clearly, we only need to prove the case that $\frac{1}{\sqrt{2}} < x < 1$. (2) is written as $$y > 2x + \ln \frac{1/x - 1}{2x - 1}. \tag{3}$$ Clearly, we only need to prove the case that $2x + \ln \frac{1/x - 1}{2x - 1} > 0$. Note that $2x + \ln \frac{1/x - 1}{2x - 1} < \sqrt{2}$ for all $\frac{1}{\sqrt{2}} < x < 1$ (easy). By Fact 2, we have $y < \sqrt{2}$.
Let $f(y) := \ln y - x \mathrm{e}^{y-2x} - (\ln 2 + \ln x - x)$. By Fact 1, we have $f'(y) > 0$ on $(0, \sqrt{2})$, given that $x \in (\frac{1}{\sqrt{2}}, \infty)$. Thus, we have $$f(y) > f\left(2x + \ln \frac{1/x - 1}{2x - 1}\right) \iff y > 2x + \ln \frac{1/x - 1}{2x - 1}$$ given that $2x + \ln \frac{1/x - 1}{2x - 1}\in (0, \sqrt{2})$, and $y \in (0, \sqrt{2})$. Using $f(y) = 0$, it suffices to prove that $$0 > f\left(2x + \ln \frac{1/x - 1}{2x - 1}\right),$$ or $$\ln \left(2x + \ln \frac{1/x - 1}{2x - 1}\right) - x \cdot \frac{1/x - 1}{2x - 1} - (\ln 2 + \ln x - x) < 0 \tag{4}$$ for all $x \in (\frac{1}{\sqrt{2}}, 1)$ with $2x + \ln \frac{1/x - 1}{2x - 1} > 0$.
Note that $- x \cdot \frac{1/x - 1}{2x - 1} - (\ln 2 + \ln x - x) < 1 - \ln 2$ for all $\frac{1}{\sqrt{2}} < x < 1$. We only need to prove the case that $\ln \left(2x + \ln \frac{1/x - 1}{2x - 1}\right) + (1 - \ln 2) \ge 0$, i.e. $2x + \ln \frac{1/x - 1}{2x - 1} \ge \frac{2}{\mathrm{e}}$ which implies $x < 4/5$. Thus, it suffices to prove (4) for $x \in (\frac{1}{\sqrt{2}}, \frac45)$.
Using $\ln (1 + u) \ge \frac{u}{2}\cdot \frac{2 + u}{1 + u}$ for all $-1 < u \le 0$, using $\frac{1/x - 1}{2x - 1} \in (0, 1)$, we have $$\ln \frac{1/x - 1}{2x - 1} \ge - \frac{(2x^2 - 2x + 1)(2x^2 - 1)}{2x(1 - x)(2x - 1)}.$$ It suffices to prove that $$g(x) := \ln \left(2x - \frac{(2x^2 - 2x + 1)(2x^2 - 1)}{2x(1 - x)(2x - 1)}\right) - x \cdot \frac{1/x - 1}{2x - 1} - (\ln 2 + \ln x - x) < 0.$$ (Note: $2x - \frac{(2x^2 - 2x + 1)(2x^2 - 1)}{2x(1 - x)(2x - 1)} > 0$ for all $x \in (\frac{1}{\sqrt{2}}, \frac45)$.)
We have $$g'(x) = \frac{(2x^2 - 1)(24x^6 - 80x^5 + 116x^4 - 102x^3 + 56x^2 - 17x + 2)}{x(1 - x)(2x - 1)^2(-12x^4 + 16x^3 - 4x^2 - 2x + 1)} < 0.$$ Also, we have $g(\frac{1}{\sqrt{2}}) = 0$. Thus, $g(x) < 0$ for all $x \in (\frac{1}{\sqrt{2}}, \frac45)$.