Lemma 11 (D1): convexity of Snl

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.relative_entropy_nonlocality_convex

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

prove2quantum

All Bell scenarios have independent finite, nonempty Alice and Bob input and output alphabets. A behavior is a nonnegative conditional output law normalized at every input pair; $\mathrm{NS}$ imposes both no-signaling marginal identities. Processing uses one initial box with rules and randomness fixed independently of the supplied behavior. Write $D(P\Vert Q)$ for classical Kullback–Leibler divergence with natural logarithms, zero numerator contributing zero and positive numerator over zero contributing $+\infty$ . Define $S_b(P\Vert Q)=\max_{x,y}D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ . For an input law $d$ , put $D_d(P\Vert Q)=\sum_{x,y}d(x,y)D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ , with zero-weight terms equal to zero. Let $\mathcal L$ be all local-hidden-variable behaviors on the same alphabets. Define $S_{\rm nl}(P)=\min_{Q\in\mathcal L}S_b(P\Vert Q)$ , $S_u(P)=\min_{Q\in\mathcal L}D_u(P\Vert Q)$ for the uniform joint law $u$ , $S_{uc}(P)=\max_{d_X,d_Y}\min_{Q\in\mathcal L}D_{d_Xd_Y}(P\Vert Q)$ , and $S_c(P)=\max_d\min_{Q\in\mathcal L}D_d(P\Vert Q)$ over all joint laws. For two no-signaling behaviors $P,Q$ on the same scenario and every real $0\le\mu\le1$ , their pointwise mixture satisfies

S_{\rm nl}(\mu P+(1-\mu)Q)\le\mu S_{\rm nl}(P)+(1-\mu)S_{\rm nl}(Q).

This is convexity in the behavior, including both endpoints. All optimizing local behaviors are selected by the defining minimization, not supplied as hypotheses.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P29

Formal statement

noncomputable section

open scoped BigOperators ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P29

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Advance50.P47
  (Box IsCorrelation IsNoSignaling HasLocalModel TwoLocalBoxes losrTransform
   correlationMixture)

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

open QAlgorithms.Papers.Independent.Dependency50.P47 (Law)

/-- PDF p.13, Lemma 11, (D1). The mixture is computed pointwise and both
endpoints of the mixing interval are included. -/
theorem relative_entropy_nonlocality_convex {s : BellScenario}
    (p q : Behavior s) (hp : IsNS p) (hq : IsNS q)
    (mu : ℝ) (hmu0 : 0 ≤ mu) (hmu1 : mu ≤ 1) :
    snl (correlationMixture p q mu) ≤
      ENNReal.ofReal mu * snl p + ENNReal.ofReal (1 - mu) * snl q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 13, Lemma 11 (D1)

Read-back

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

Let $s$ be any Bell scenario, with finite nonempty question sets $X,Y$ and answer sets $A,B$ , and let $p,q:X\times Y\times A\times B\to\mathbb R$ be nonnegative arrays satisfying $\sum_{a,b}p(x,y,a,b)=\sum_{a,b}q(x,y,a,b)=1$ for every $x,y$ . Assume each array has Bob’s marginal independent of Alice’s question and Alice’s marginal independent of Bob’s question. For probability arrays $r,t$ on a finite set, define $D(r\|t)=+\infty$ if some coordinate has $r_i>0$ and $t_i=0$ , and otherwise define $D(r\|t)=\max\{0,\sum_i r_i\log(r_i/t_i)\}$ , viewed in $[0,+\infty]$ , using natural logarithms and the total real operations $x/0=0$ and $\log 0=0$ . Let $\mathcal L_s$ consist of the nonnegative normalized arrays $\ell$ admitting a representation $\ell(x,y,a,b)=\sum_h \pi(h)A_h(a\mid x)B_h(b\mid y)$ , where the hidden-variable set is arbitrary, $\pi$ is a discrete probability mass function, and every $A_h(\cdot\mid x)$ and $B_h(\cdot\mid y)$ is a nonnegative probability distribution. Define

N(r)=\inf_{\ell\in\mathcal L_s}\ \sup_{x\in X,y\in Y} D\bigl(r(x,y,\cdot,\cdot)\,\|\,\ell(x,y,\cdot,\cdot)\bigr).

For every real $\mu$ with $0\le\mu\le1$ , the pointwise mixture $r=\mu p+(1-\mu)q$ satisfies $N(r)\le\mu N(p)+(1-\mu)N(q)$ . This includes $\mu=0,1$ ; the inequality uses extended nonnegative arithmetic, with $0\cdot(+\infty)=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