Return to Answer

$\newcommand{\ep}{\varepsilon}$ The proposed bounds are simple and remarkably tight. We shall prove them by considering separately the cases of large, small, and intermediate values of $a$.

All and, in particular, large values of $a$. Let \begin{equation*} g(x):=x^2-x-\ln x \end{equation*} for $x>0$. Then $g(1)=g'(1)=0$ and $g$ is strictly convex, with $g(0+)=g(\infty-)=\infty$. So, $g$ is strictly decreasing from $\infty$ to $0$ on $(0,1]$ and strictly increasing from $0$ to $\infty$ on $[1,\infty)$. So, for each real $a>0$ there are uniquely determined $x_1=x_1(a)\in(0,1)$ and $x_2=x_2(a)\in(1,\infty)$ such that \begin{equation*} g(x_1)=g(x_2)=\ln a; \end{equation*} of course, these $x_1$ and $x_2$ are the same as in the OP.

Intermediate values of a. In view of the above considerations of large and small values of $a$, it remains to prove the lower bound $\frac3{2a+1}$ on $x_1x_2$ for $a\in[1+\tfrac{175}{1000},11]$ and the lower bound $\frac{\ln a}{a-1}$ on $x_1x_2$ for $a\in[1+\tfrac{127}{1000},17]$. This is done by the interval method, by partitioning these intervals of values of $a$ into many small subintervals and bounding $x_1x_2$ and the corresponding bounds on each small subinterval. Note that the monotonicity pattern of the function $g$ allows one to approximate the values of $x_1$ and $x_2$ with any prescribed degree of accuracy, for each $a>1$. However, here it is slightly more convenient to use the explicit (albeit very complicated) equivalent form of the inequalities in question, given in the last display in the OP: \begin{equation*} \frac3{2e^{g(F(t))}+1}< t F(t)^2<\frac{g(F(t))}{e^{g(F(t))}-1}, \tag{1} \end{equation*} where \begin{equation*} F(t):=\frac{t-1+\sqrt{(t-1)^2+4\ln{t}\cdot(t^2-1)}}{2(t^2-1)}=x_1\in(0,1) \end{equation*} and $t:=t(a):=x_2/x_1>1$. (The OP used the symbol $f$ to denote both $F$ and $g(x)-\ln a$.)

$\newcommand{\ep}{\varepsilon}$ Each of the two proposed inequalities can be written in the form $H(a)>0$ for $a\in(1,\infty)$, where $H$ is a smooth function. All such inequalities -- but only for $a$ in a finite closed interval $I$ -- can be proved, at least in principle, by the interval method; that is, by partitioning $I$ into many small subintervals and bounding, tightly enough, terms in the expression of $H(a)$ on each small subinterval. A difficulty of using the interval method here is that $x_1$ and $x_2$ as functions of $a$ are known only implicitly. Another difficulty is that the interval $I$ is neither finite nor closed, and so, we shall need to consider separately ("small") values of $a$ close to $1+$ and large values of $a$, close enough to $\infty$. For intermediate values of $a$, we shall indeed use the interval method.

Therefore, the solution presented below is long and technical. Since the problem does not seem to belong to a general class of problems, I'd be surprised if there is an "official" solution to it.

All and, in particular, large values of $a$. Let \begin{equation*} g(x):=x^2-x-\ln x \end{equation*} for $x>0$. Then $g(1)=g'(1)=0$ and $g$ is strictly convex, with $g(0+)=g(\infty-)=\infty$. So, $g$ is strictly decreasing from $\infty$ to $0$ on $(0,1]$ and strictly increasing from $0$ to $\infty$ on $[1,\infty)$. So, for each real $a>0$ there are uniquely determined $x_1=x_1(a)\in(0,1)$ and $x_2=x_2(a)\in(1,\infty)$ such that \begin{equation*} g(x_1)=g(x_2)=\ln a; \end{equation*} of course, these $x_1$ and $x_2$ are the same as in the OP.

Intermediate values of a. In view of the above considerations of large and small values of $a$, it remains to prove the lower bound $\frac3{2a+1}$ on $x_1x_2$ for $a\in[1+\tfrac{175}{1000},11]$ and the lower bound $\frac{\ln a}{a-1}$ on $x_1x_2$ for $a\in[1+\tfrac{127}{1000},17]$. This is done by the mentioned interval method. Note that the monotonicity pattern of the function $g$ allows one to approximate the values of $x_1$ and $x_2$ with any prescribed degree of accuracy, for each $a>1$. However, here it is slightly more convenient to use the explicit (albeit very complicated) equivalent form of the inequalities in question, given in the last display in the OP: \begin{equation*} \frac3{2e^{g(F(t))}+1}< t F(t)^2<\frac{g(F(t))}{e^{g(F(t))}-1}, \tag{1} \end{equation*} where \begin{equation*} F(t):=\frac{t-1+\sqrt{(t-1)^2+4\ln{t}\cdot(t^2-1)}}{2(t^2-1)}=x_1\in(0,1) \end{equation*} and $t:=t(a):=x_2/x_1>1$. (The OP used the symbol $f$ to denote both $F$ and $g(x)-\ln a$.)

Since $t$ is increasing and $x_1=F(t)$ is decreasing in $a$, it follows that $F(t)\in(0,1)$ is decreasing in $t>1$. Therefore and because $g$ is decreasing on $(0,1)$, $g(F(t))$ is increasing in $t$. Also, $\frac b{e^b-1}$ is decreasing in $b>0$. So, \begin{equation*} \frac{g(F(t))}{e^{g(F(t))}-1} \end{equation*} is decreasing in $t>1$. So, to prove the second inequality in (1) for $a\in[1+\tfrac{127}{1000},17]$, it suffices to show that \begin{equation*} t_{j+1} F(t_j)^2<\frac{g(F(t_{j+1}))}{e^{g(F(t_{j+1}))}-1} \end{equation*} for all integers $j\in\{0,\dots,53n\}$, where $n=300$, $t_j:=\frac{176}{100}+\frac jn$, so that $t_{53n}=53+\frac{176}{100}\ge53.974\ldots$. This is done by straightforward calculation (taking about 14 sec with Mathematica).

Since $t$ is increasing and $x_1=F(t)$ is decreasing in $a$, it follows that $F(t)\in(0,1)$ is decreasing in $t>1$. Therefore and because $g$ is decreasing on $(0,1)$, $g(F(t))$ is increasing in $t$. Also, $\frac b{e^b-1}$ is decreasing in $b>0$. So, \begin{equation*} \frac{g(F(t))}{e^{g(F(t))}-1} \end{equation*} is decreasing in $t>1$. So, to prove the second inequality in (1) for $a\in[1+\tfrac{127}{1000},17]$, it suffices to show that \begin{equation*} t_{j+1} F(t_j)^2<\frac{g(F(t_{j+1}))}{e^{g(F(t_{j+1}))}-1} \tag{2} \end{equation*} for all integers $j\in\{0,\dots,53n\}$, where $n=300$, $t_j:=\frac{176}{100}+\frac jn$, so that $t_{53n}=53+\frac{176}{100}\ge53.974\ldots$. Indeed, then it will follow that \begin{equation*} t F(t)^2\le t_{j+1} F(t_j)^2<\frac{g(F(t_{j+1}))}{e^{g(F(t_{j+1}))}-1} \le\frac{g(F(t))}{e^{g(F(t))}-1} \end{equation*} for all $j\in\{0,\dots,53n\}$ and all $t\in[\frac{176}{100}+\frac jn,\frac{176}{100}+\frac{j+1}n]$, so that we will indeed have the second inequality in (1) for all $t\in[t(1+\tfrac{127}{1000}),t(17)]$. The proof of (2) is done by straightforward calculation (taking about 14 sec with Mathematica).

The conditions $g(x_2)=\ln a$ and $x_2>1$ yield $x_2^2=x_2+\ln x_2+\ln a\ge 1+\ln a$, so that we get a lower bound on $x_2$: \begin{equation*} x_2>X_2^{lo}:=X_2^{lo}(a):=\sqrt{1+\ln a}. \end{equation*} Therefore and because $h(x):=\frac{x+\ln x}{x^2}$ is decreasing in $x\ge1$ (from $1$ to $0$), we have $h(x_2)<h(\sqrt{1+\ln a})\le h(\sqrt{1+\ln 17})$ if $a\ge17$. So, $x_2^2=h(x_2)x_2^2+\ln a<h(\sqrt{1+\ln 17})x_2^2+\ln a$, and we get an upper bound on $x_2$: \begin{equation*} x_2<X_2^{up}:=X_2^{up}(a):=\frac{\sqrt{\ln a}}c \end{equation*} for $a\ge17$, where $c:=\sqrt{1-h(\sqrt{1+\ln 17})}\approx0.560$.

The conditions $g(x_2)=\ln a$ and $x_2>1$ yield $x_2^2=x_2+\ln x_2+\ln a\ge 1+\ln a$, so that we get a lower bound on $x_2$: \begin{equation*} x_2>X_2^{lo}:=X_2^{lo}(a):=\sqrt{1+\ln a}. \end{equation*} Therefore and because $h(x):=\frac{x+\ln x}{x^2}$ is decreasing in $x\ge1$ (from $1$ to $0$), we have $h(x_2)<h(\sqrt{1+\ln a})\le h(\sqrt{1+\ln 17})$ if $a\ge17$. So, $x_2^2=h(x_2)x_2^2+\ln a<h(\sqrt{1+\ln 17})x_2^2+\ln a$, and we get an upper bound on $x_2$: \begin{equation*} x_2<X_2^{up}:=X_2^{up}(a):=\frac{\sqrt{\ln a}}c \quad\text{for}\quad a\ge17, \end{equation*} where $c:=\sqrt{1-h(\sqrt{1+\ln 17})}\approx0.560$.