§V-B, unnumbered monotonicity of optimized exponents

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.exponent_monotonicity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $S,X,Y,Z$ be finite nonempty alphabets and let $W(x,y,z\mid s)$ be a normalized discrete memoryless broadcast channel. All entropies and information quantities are in bits. For an input law $p$ , information quantities below use exactly the induced law $p(s)W(x,y,z\mid s)$ .

Alice draws a uniform finite message $M$ , uses a possibly stochastic encoder to excite $n$ channel uses, and observes $(M,X^n)$ . A public forward message $\Phi=\phi(M,X^n)$ is visible to Bob and Eve. Their keys are $K_A=k_A(M,X^n)$ and $K_B=k_B(Y^n,\Phi)$ . All design maps are fixed publicly before observations. Message and public alphabets follow the fixed-rate ceiling convention; the key alphabet at rate $R$ has exactly $2^{\lceil nR\rceil}$ labels. A weakly achievable rate $R$ has one sequence of such codes with disagreement tending to zero, $I(K_A;Z^n,\Phi)/n\to0$ , and $\liminf H(K_A)/n\ge R$ .

There is no excitation cost constraint. Rates and target exponents are nonnegative. Let $\mathcal R$ be the closure of triples $(R,E,F)$ attained by a single code sequence satisfying the entropy-rate lower bound and $\liminf[-\log_2\Pr(K_A\ne K_B)]/n\ge E$ , $\liminf[-\log_2 I(K_A;Z^n,\Phi)]/n\ge F$ . A zero error or leakage has decay rate $+\infty$ . Strong achievability requires both $E>0$ and $F>0$ .

For $0\le\rho\le1$ put

e_1(\rho)=\rho R_\Phi-\log_2\sum_{s,y}p(s)W_Y(y\mid s)\left[\sum_x W_{X\mid Y,S}(x\mid y,s)^{1/(1+\rho)}\right]^{1+\rho},

e_2(\rho)=\rho(R_\Phi-R_M)-\log_2\sum_{x,y}\left[\sum_s p(s)W_{XY}(x,y\mid s)^{1/(1+\rho)}\right]^{1+\rho},

e_3(\rho)=\rho(R_\Phi-R_M)-\log_2\sum_y\left[\sum_{s,x}p(s)W_{XY}(x,y\mid s)^{1/(1+\rho)}\right]^{1+\rho}.

Let $E_o=\min_{j=1,2,3}\max_{\rho\in[0,1]} e_j(\rho)$ . Here $W_{XY}$ and $W_Y$ are the indicated channel marginals. Unsupported conditional rows have zero outer weight. The first and second displays incorporate the documented source corrections C18 and C19.

For $0<\alpha\le1$ put

f(\alpha)=-\alpha(R_{\rm SK}+R_\Phi-R_M)-\log_2\sum_{s,x,z}p(s)W_{XZ}(x,z\mid s)\left[\frac{W_{XZ}(x,z\mid s)}{p_Z(z)}\right]^\alpha, \qquad F_o=\sup_{0<\alpha\le1}f(\alpha).

Here $p_Z$ is induced by $p$ and $W$ , and null $z$ fibers contribute zero.

Let $E_r(R_\Phi,R_M)=\sup_p E_o(p,R_\Phi,R_M)$ and $F_r(R_{\rm SK},R_\Phi,R_M)=\sup_p F_o(p,R_{\rm SK},R_\Phi,R_M)$ , independently optimized over normalized input laws. On nonnegative rates,

E_r\text{ is nondecreasing in }R_\Phi\text{ and nonincreasing in }R_M;

F_r\text{ is nonincreasing in }R_\Phi,\text{ nondecreasing in }R_M,\text{ and nonincreasing in }R_{\rm SK}.

The optimizing input laws need not coincide, so this does not assert joint achievability of the independently optimized pair.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P76

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P76

noncomputable section

open scoped BigOperators

open Filter Set

attribute [local instance] Classical.propDecidable

-- Exact pinned primitives, inspected at their definitions before reuse.

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Frontier30.P12 (IsStochastic)

variable {S X Y Z : Type} [Fintype S] [Fintype X] [Fintype Y] [Fintype Z]
  [Nonempty S] [Nonempty X] [Nonempty Y] [Nonempty Z]

variable {n u w : ℕ}

/-- PDF pp.9--10: all five monotonicity clauses. Separate optimizers need
not coincide, so their pair is not asserted operationally achievable. -/
theorem exponent_monotonicity (W : DMBC S X Y Z) :
    (∀ RM : ℝ, 0 ≤ RM → MonotoneOn (fun RP => optimizedReliability W RP RM) (Ici 0)) ∧
    (∀ RP : ℝ, 0 ≤ RP → AntitoneOn (fun RM => optimizedReliability W RP RM) (Ici 0)) ∧
    (∀ RK RM : ℝ, 0 ≤ RK → 0 ≤ RM →
      AntitoneOn (fun RP => inputOptimizedSecrecyExponent W RK RP RM) (Ici 0)) ∧
    (∀ RK RP : ℝ, 0 ≤ RK → 0 ≤ RP →
      MonotoneOn (fun RM => inputOptimizedSecrecyExponent W RK RP RM) (Ici 0)) ∧
    (∀ RP RM : ℝ, 0 ≤ RP → 0 ≤ RM →
      AntitoneOn (fun RK => inputOptimizedSecrecyExponent W RK RP RM) (Ici 0)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P76

Source

The Sender-Excited Secret Key Agreement Model: Capacity, Reliability and Secrecy Exponents, arXiv:1107.4148v4, PDF p. 9, §V-B, unnumbered monotonicity of optimized exponents

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every $W$ on finite, nonempty alphabets $S,X,Y,Z$ , with $w_s(x,y,z)\ge0$ and $\sum_{x,y,z}w_s(x,y,z)=1$ for each $s$ , define $a_s(x,y)=\sum_z w_s(x,y,z)$ , $b_s(y)=\sum_x a_s(x,y)$ , $c_s(x,z)=\sum_y w_s(x,y,z)$ , and $q_p(z)=\sum_{s,x}p(s)c_s(x,z)$ . Let $\mathcal P(S)$ consist of all nonnegative real functions on $S$ summing to one, and define the extended-real functions

\begin{aligned} \mathcal R(R_P,R_M) =\sup_{p\in\mathcal P(S)}\min\Bigg\{& \sup_{\rho\in[0,1]} \left[\rho R_P-\log_2\sum_{s,y}p(s)b_s(y) \left(\sum_x\left(\frac{a_s(x,y)}{b_s(y)}\right)^{1/(1+\rho)}\right)^{1+\rho}\right],\\ &\sup_{\rho\in[0,1]} \left[\rho(R_P-R_M)-\log_2\sum_{x,y} \left(\sum_s p(s)a_s(x,y)^{1/(1+\rho)}\right)^{1+\rho}\right],\\ &\sup_{\rho\in[0,1]} \left[\rho(R_P-R_M)-\log_2\sum_y \left(\sum_{s,x}p(s)a_s(x,y)^{1/(1+\rho)}\right)^{1+\rho}\right] \Bigg\}, \end{aligned}

and

\mathcal S(R_K,R_P,R_M)= \sup_{p\in\mathcal P(S)}\sup_{\alpha\in(0,1]} \left[-\alpha(R_K+R_P-R_M) -\log_2\sum_z \begin{cases} 0,&q_p(z)=0,\\ \displaystyle\sum_{s,x}p(s)c_s(x,z) \left(\frac{c_s(x,z)}{q_p(z)}\right)^\alpha,&q_p(z)\ne0. \end{cases}\right],

with every bracketed real value embedded into the extended reals. The theorem asserts all five inequalities

\begin{aligned} \mathcal R(u,R_M)&\le\mathcal R(v,R_M) &&\text{if }R_M\ge0,\quad 0\le u\le v,\\ \mathcal R(R_P,v)&\le\mathcal R(R_P,u) &&\text{if }R_P\ge0,\quad 0\le u\le v,\\ \mathcal S(R_K,v,R_M)&\le\mathcal S(R_K,u,R_M) &&\text{if }R_K,R_M\ge0,\quad 0\le u\le v,\\ \mathcal S(R_K,R_P,u)&\le\mathcal S(R_K,R_P,v) &&\text{if }R_K,R_P\ge0,\quad 0\le u\le v,\\ \mathcal S(v,R_P,R_M)&\le\mathcal S(u,R_P,R_M) &&\text{if }R_P,R_M\ge0,\quad 0\le u\le v. \end{aligned}

All boundary values, including zero rates and zero probability masses, are included; division by zero is zero, and the total real logarithm has $\log_2 0=0$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph