请求证明涉及log cosh的不等式（用于独立随机变量混合解混/去卷积的稳定最优解唯一性）

大家好，我目前卡在了一个不等式的证明上，想请各位帮忙梳理下思路。首先给出待证的核心不等式：当$y>x\ge 0$时，

$$\bigg(\frac{y^2-x2}{\cosh^2(x)}-x\tanh(x)-y\tanh(y)!\bigg)\log!\bigg(\frac{\cosh(y)}{\cosh(x)}\bigg) + \tanh^2(x)\big(y2-x^2\big) > 0 $$

背景说明 #

这个不等式对独立随机变量线性混合的解混与去卷积问题中稳定最优解的唯一性证明至关重要，核心用到了具有单调似然比的密度的变分递减性质。本质上，它等价于相关密度函数满足$\frac{\partial}{\partial x}\frac{\partial}{\partial y},\log f(x,y)<0$这个条件。

已尝试的思路 #

我已经验证过两个相关函数的凸凹性：

• $\log(\cosh(x))$是凸函数
• $\log(\cosh(\sqrt{x}))$在$[0,\infty)$上是凹函数

但用这两个函数对应的凸/凹不等式，都没法推导得到目标结论。

当前进展 #

后来我尝试用一个下界估计：
$$\log(\cosh(y))-\log(\cosh(x)) \ge \sqrt{y^2+1}-\sqrt{x2+1}$$
只保留原式中的正项$\frac{y^2-x2}{\cosh^2(x)}$，将$\log \cosh$相关项分离出来，转化得到了一个新的待证不等式（同样要求$y>x\ge 0$）：
$$\frac{\big(\sqrt{y^2+1}-\sqrt{x2+1}+\sinh^{2(x)\big)\big(y}2-x^{2\big)}{\cosh}2(x)\big(x\tanh(x)+y\tanh(y)\big)} - \log!\bigg(\frac{\cosh(y)}{\cosh(x)}\bigg) ;>; 0$$

我观察到这个新表达式关于$y$是递增的，理论上对$y$求导可以消去$\log \cosh$项，只要能证明求导后的结果非负，就能完成原不等式的证明。但求导后得到的表达式极其复杂，看起来比原问题更难处理，卡在这里了。

有没有大佬能给点思路或者方向呀？

备注：内容来源于stack exchange，提问作者japalmer