Metadata

slug: hirche-2020-cachin-renyi-information-combining-convexity
bibkey: hirche2020renyibounds
doi: 10.48550/arXiv.2004.14408
url: https://arxiv.org/abs/2004.14408v1
triage: theorem
motivation_gids:
  - D5/S3/Entropy/RenyiCombining/HircheCachinCombiningConcavity.result

Cachin Rényi information combining convexity and concavity

Problem

The target is the whole of C. Hirche, “Rényi Bounds on Information Combining”, ISIT 2020, arXiv:2004.14408v1, §IV-D, Conjecture IV.18, Eq. (88):

There exists a value $1 < \overset{α}{^} < 1.3863$ , such that $h_{α} (h_{α}^{- 1} (x) * h_{α}^{- 1} (y))$ is convex for $0 < α < \overset{α}{^}$ and concave for $α \geq 2$ .

The formal claim supplies the witness $\overset{α}{^} = 5/4$ and quantifies over every fixed $y \in [0, lo g 2]$ , with convexity or concavity in $x$ on the whole closed entropy interval. Put

$h_{α} (p) = {- p lo g p - (1 - p) lo g (1 - p), lo g (p^{α} + (1 - p)^{α}) / (1 - α), α = 1, α \neq = 1, p ⋆ q = p + q - 2 pq .$

The inverse branch has probability domain $[0, 1/2]$ . Logarithms are natural, all orders are real, and the Shannon value is Mathlib’s Real.binEntropy.

This provides the scalar convexity and concavity inputs for binary Rényi information combining. The convexity interval crosses the Shannon order, and concavity quantifies over every real order at least two. Both statements include entropy endpoints.

Gap

No independent literature or priority search is claimed. The exact maximal convexity threshold and quantum conditional-entropy inequalities are outside the formal target.

Route

Put $ψ (t) = h_{α} ((1 - t) /2)$ , $n = α - 1$ and $r (t) = (1 - t) / (1 + t)$ . For $0 < r < 1$ , let

$T = \frac{1 - r ^{n}}{1 + r ^{n}}, A = \frac{n r ^{n - 1} ( 1 - r ^{2} )}{1 - r ^{2 n}}, B = \frac{1 - r}{1 + r} T, F = \frac{A - B}{1 + B} .$

For $n \geq 1$ , the certificate proves that $F$ is increasing. Its nonnegative derivative uses $J_{n} (z) = (n - 1) - (n + 1) z + (n + 1) z^{n} - (n - 1) z^{n + 1} \geq 0$ , obtained by two applications of derivative-sign monotonicity on $[z, 1]$ with $z > 0$ . For $f = - ψ^{'} > 0$ , differentiation gives $f^{'} = f F (r (t)) / t$ . Consequently $v f (v t) / f (t)$ increases in $t$ for $0 < v < 1$ . The inverse of $ψ$ decreases, so the first derivative of the transported combining function decreases in its entropy input. Continuity gives concavity on the closed interval. The cases $v = 0$ and $v = 1$ are respectively a constant and the identity. No endpoint inverse derivative is required.

For $- 1 < n < 0$ , the shared derivatives give $A^{'} \leq 0$ , $B^{'} > 0$ , $A > 0$ and $- 1 < B < 0$ , so $F^{'} < 0$ . At the Shannon order, $- ψ_{1}^{'} (t) = artanh (t)$ and $E_{1} (t) = t / ((1 - t^{2}) artanh (t))$ increases because $artanh (t) \geq t$ .

For $0 < n \leq 1/4$ , the auxiliary quotient $C_{n}$ and $D_{n} = C_{n} + n z$ satisfy the Riccati equations below. An even analytic quotient in $t$ removes the singularity before substituting $z = t^{2}$ . Its second and fourth derivatives at zero give local negative curvature. The first-zero argument then gives $C_{n}^{''} < 0$ on $(0, 1)$ and $D_{n}^{'} < 0$ , so $1 - 2 z D_{n}^{'} / D_{n}$ is strictly increasing. This equals $F_{n} ((1 - t) / (1 + t))$ at $z = t^{2}$ . The same inverse transport therefore gives convexity, with the derivative sign reversed.

The reuse boundary is:

Needed interface	Reused source	Role
Binary Shannon entropy and derivative	Mathlib `Real.binEntropy`, `Real.hasDerivAt_binEntropy`	The order-one definition and bias derivative
Inverse hyperbolic tangent	`ContractionSpectrumOrder.hasDerivAt_artanh`; Mathlib `Real.artanh_eq_half_log`, `Real.artanh_pos`, `Real.sum_range_le_log_div`	The logarithmic and Shannon derivatives share one source; the one-term logarithm bound gives artanh(t) ≥ t
Binary Rényi entropy and convolution	`RenyiInformationCombiningOrderThree.hRenyi`, `bconv`, `bconv_bias`	Non-Shannon entropy, convolution and the bias product identity
Inverse branch and continuity	Mathlib `Function.invFunOn_mem`, `Function.invFunOn_eq`, `Set.InjOn.leftInvOn_invFunOn`, `Continuous.continuous_symm_of_equiv_compact_to_t2`	The specified probability inverse and continuity on the closed entropy interval
Hyperbolic quotient and derivatives	Mathlib `Real.cosh`, `Real.sinh`, `Real.cosh_sq_sub_sinh_sq` and derivative composition	The Riccati quotient uses explicit cosh/sinh in place of a coth interface
Real-power derivatives and binomial series	Mathlib `Real.hasDerivAt_rpow_const`, `Real.one_add_rpow_hasFPowerSeriesAt_zero`	Negative orders and removable initial quotient
Analytic removable division	Mathlib `HasFPowerSeriesAt.has_fpower_series_dslope_fslope`	Initial Taylor coefficients
First-zero selection and mean value theorem	Mathlib `IsCompact.exists_isLeast`, derivative-sign monotonicity	Global negative curvature
Closed-interval convexity	Mathlib `MonotoneOn.convexOn_of_deriv`; `convexOn_of_deriv2_nonneg` is also available	The first-derivative criterion transports through the continuous inverse without a separate second derivative of G
Real-order elasticity and inverse transport	Existing `CachinElasticityMonotone` and main-module infrastructure	Shared functions, derivatives and probability branch

Falsifier

A violation to the witness theorem consists of a permitted $y$ , two entropy points and a convex weight, violating convexity at some $0 < α < 5/4$ or concavity at some $α \geq 2$ . A source mismatch or a prior settlement would affect the source or novelty claim independently of kernel verification.

Evidence

The settling declaration is result : claim in D5/S3/Entropy/RenyiCombining/HircheCachinCombiningConcavity.lean. The real-power, Shannon, analytic-initial-data and Riccati certificates are used on the live proof path. The inverse identities are proved for the specified probability branch. The settling declaration has axiom closure contained in propext, Classical.choice, and Quot.sound.

Triage

The complete source conjecture reads: “There exists a value $1 < \overset{α}{^} < 1.3863$ , such that $h_{α} (h_{α}^{- 1} (x) * h_{α}^{- 1} (y))$ is convex for $0 < α < \overset{α}{^}$ and concave for $α \geq 2$ .” The formalized scope is this entire assertion with witness $\overset{α}{^} = 5/4$ . The settling result combines convexity for every $0 < α < 5/4$ with concavity for every $α \geq 2$ , including the Shannon order and all entropy endpoints.

The exact separate-convexity threshold

$α_{c} = \frac{13 - 1}{2}$

is proved on paper, not formalized. With $n = α - 1$ , $C_{n} (z) = n z coth (n artanh z)$ (with the continuous $n = 0$ and $z = 0$ values) satisfies

$2 z (1 - z) C_{n}^{'} = (1 - z) C_{n} - C_{n}^{2} + n^{2} z .$

Its initial derivatives are $C_{n}^{'} (0) = - (1 - n^{2}) /3$ and $C_{n}^{''} (0) = - 2 (1 - n^{2}) (4 - n^{2}) /45$ . Differentiating the Riccati equation twice gives

$2 z (1 - z) C_{n}^{'''} = (- 3 + 7 z - 2 C_{n}) C_{n}^{''} + 2 C_{n}^{'} (1 - C_{n}^{'}) .$

A first zero of $C_{n}^{''}$ would have nonnegative derivative, while this identity makes that derivative negative because $C_{n}^{'} < 0$ . Thus $C_{n}^{''} < 0$ . For $D_{n} = C_{n} + n z$ and $- 1 < n \leq (13 - 3) /2$ , its initial slope $D_{n}^{'} (0) = (n^{2} + 3 n - 1) /3 \leq 0$ and its negative curvature imply $D_{n}^{'} < 0$ . Since $D_{n} > 0$ , the elasticity $E_{α} (t) = 1 - 2 t^{2} D_{n}^{'} (t^{2}) / D_{n} (t^{2})$ is strictly increasing. The inverse entropy transport then gives separate convexity, including the threshold. The local expansion

$E_{α} (t) = 1 + \frac{2 ( 3 - α - α ^{2} )}{3} t^{2} + O (t^{4})$

makes the elasticity decrease near zero when $α > α_{c}$ , excluding separate convexity there. This expansion and the exact threshold are not claimed as kernel-verified conclusions.

The interval $(α_{c}, 2)$ lies between the two convexity/concavity regimes. Lemma IV.16 of the paper shows neither convexity nor concavity on $(1.387, 1.95)$ . That lemma does not by itself settle concavity throughout $(α_{c}, 2)$ ; the local expansion excludes convexity above $α_{c}$ , and a concavity classification of the remaining orders is not asserted here.

ASSUMED-UNVERIFIED

The paper locator and the absence of a later settlement have not been independently verified against later literature. The formal theorem has no mathematical premise asserting the conjecture or its elasticity inequality.

trureturing — Discovering truth