I'm trying to prove this messy inequality I got while working on an information theoretic problem (more details below).

Let $0 \leq p,q \leq \frac{1}{2}$.

Let $H(x) = -x\log(x) - (1-x)\log(1-x)$ be the binary entropy function.

Let $p\star q = p(1-q) +q(1-p)$ (think of this as addition of two Bernoulli random variables in $\mathbb{Z}_2$)

The inequality is: $$-\frac{(1-2q)}{(p \star q) (1- p \star q)\log\left(\frac{1-p}{p}\right)} + \frac{\log\left(\frac{1- p \star q}{p \star q}\right)}{p(1-p)\left(\log\left(\frac{1-p}{p}\right)\right)^2} - \frac{H(q)(1-2p)}{H(p)(p \star q) (1- p \star q)\log\left(\frac{1-q}{q}\right)} \leq 0$$

Some Remarks:

If we write this as $-A+B-C \leq 0$ with $A,B,C$ being the corresponding quantities above. I can show that $-A +B \geq 0$, so the $-C$ term subtracts enough to make the expression negative. The plot of $-A+B-C$ as a function of $p,q$ looks like

.

It appears to decrease in $q$ for a fixed $p$, starting at $0$ and going to $-\infty$ as $q$ goes to $\frac{1}{2}$.

Origin:
This inequality came from looking at a function $f(x,y) = H(H^{-1}(x)\star H^{-1}(y))$ where $f: [0,1]\times [0,1] \to [0,1]$. This function occasionally pops up in information theory, like when studying the binary symmetric channel or an inequality called Mrs. Gerber's Lemma. The inequality I have implies that $f(x,y)$ is concave along lines through the origin (i.e $f(x,\theta x)$ is concave in $x$). What I've written is a simplified version $f''$ along a line through the origin.

I'm at a complete loss as to how to attack this. All the plots I have show this is true, but a plot is not a proof. Any suggestions welcome!

EDIT:
After much work I was able to reduce the inequality to a single variable function which I need to show is non-positive. That function is (for $0\leq p\leq\frac{1}{2}$) $$\frac{p^2(\log(p))^2 - (1-p)^2(\log(1-p))^2}{1-2p} + \log(p)\log(1-p) + p\log(p)+(1-p)\log(1-p) \leq 0$$ This looks tractable, but is quite hard to prove since neither the function nor any of its derivatives are convex/concave/monotonic. Its graph looks like

.

Any inputs welcome!

END EDIT

I'm trying to prove this messy inequality I got while working on an information theoretic problem (more details below).

Let $0 \leq p,q \leq \frac{1}{2}$.

Let $H(x) = -x\log(x) - (1-x)\log(1-x)$ be the binary entropy function.

Let $p\star q = p(1-q) +q(1-p)$ (think of this as addition of two Bernoulli random variables in $\mathbb{Z}_2$)

The inequality is: $$-\frac{(1-2q)}{(p \star q) (1- p \star q)\log\left(\frac{1-p}{p}\right)} + \frac{\log\left(\frac{1- p \star q}{p \star q}\right)}{p(1-p)\left(\log\left(\frac{1-p}{p}\right)\right)^2} - \frac{H(q)(1-2p)}{H(p)(p \star q) (1- p \star q)\log\left(\frac{1-q}{q}\right)} \leq 0$$

Some Remarks:

If we write this as $-A+B-C \leq 0$ with $A,B,C$ being the corresponding quantities above. I can show that $-A +B \geq 0$, so the $-C$ term subtracts enough to make the expression negative. The plot of $-A+B-C$ as a function of $p,q$ looks like

.

It appears to decrease in $q$ for a fixed $p$, starting at $0$ and going to $-\infty$ as $q$ goes to $\frac{1}{2}$.

Origin:
This inequality came from looking at a function $f(x,y) = H(H^{-1}(x)\star H^{-1}(y))$ where $f: [0,1]\times [0,1] \to [0,1]$. This function occasionally pops up in information theory, like when studying the binary symmetric channel or an inequality called Mrs. Gerber's Lemma. The inequality I have implies that $f(x,y)$ is concave along lines through the origin (i.e $f(x,\theta x)$ is concave in $x$). What I've written is a simplified version $f''$ along a line through the origin.

I'm at a complete loss as to how to attack this. All the plots I have show this is true, but a plot is not a proof. Any suggestions welcome!