Manuscript Oai276-A@1 · Oai276-A.tex · lemma · 215068af

Lemma: Strict derivative and quantitative curvature

Stages 3 and 6: the explicit finite maximum certificate › Freeze a genuinely thermal, nonunital channel · lines 865–918 · proof included or linked

Oai276-A@1#lem:derivative, Oai276-A@1#eq:D, Oai276-A@1#eq:curvature, Oai276-A@1#eq:quadratic

For the frozen channel, $f$ is smooth on $[0, 1]$ and

D (p) := f^{'} (p) = atanh (x (p)) - d (p) \frac{atanh q ( p )}{q ( p )} .

Moreover,

f^{''} (p) \leq - 1 (0 \leq p \leq 1) .

Consequently $D$ is strictly decreasing and, for every $p_{0}$ ,

p \in [0, 1] max f (p) \leq f (p_{0}) + \frac{D ( p _{0} ) ^{2}}{2} .

Proof. The output population lies in $[1/8, 5/8]$ . The determinant is strictly between zero and $1/4$ , so all functions used here are smooth.

For $r = 1 - 4 u$ ,

g_{e}^{'} (u) = \frac{1}{r} ln \frac{1 + r}{1 - r} .

Differentiate (eq:f) and use $1 - 2 (p /2 + 1/8) = x (p)$ to obtain (eq:D).

The determinant entropy term is convex by Lemma lem:convex. For the first term,

\frac{d ^{2}}{d p ^{2}} h_{e} (\frac{p}{2} + \frac{1}{8}) = - \frac{1}{4 t ( p ) ( 1 - t ( p ))} \leq - 1.

This proves (eq:curvature).

Integrating the curvature bound gives

f (p) \leq f (p_{0}) + D (p_{0}) (p - p_{0}) - \frac{1}{2} (p - p_{0})^{2} .

The maximum of the quadratic on the whole real line is $f (p_{0}) + D (p_{0})^{2} /2$ , proving (eq:quadratic).

Displayed formulas in this passage

Oai276-A@1#eq:D · line 868
$D (p) := f^{'} (p) = atanh (x (p)) - d (p) \frac{atanh q ( p )}{q ( p )} .$
Oai276-A@1#eq:curvature · line 877
$f^{''} (p) \leq - 1 (0 \leq p \leq 1) .$
Oai276-A@1#eq:quadratic · line 883
$p \in [0, 1] max f (p) \leq f (p_{0}) + \frac{D ( p _{0} ) ^{2}}{2} .$
unlabeled · line 897
$g_{e}^{'} (u) = \frac{1}{r} ln \frac{1 + r}{1 - r} .$
unlabeled · line 905
$\frac{d ^{2}}{d p ^{2}} h_{e} (\frac{p}{2} + \frac{1}{8}) = - \frac{1}{4 t ( p ) ( 1 - t ( p ))} \leq - 1.$
unlabeled · line 913
$f (p) \leq f (p_{0}) + D (p_{0}) (p - p_{0}) - \frac{1}{2} (p - p_{0})^{2} .$