Entropic steering inequality for two observed marginals

Open

QAlgorithms.Papers.Independent.Intakethird100.P94.entropicSteering_S5

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

prove2quantum

Let $P(a,s,b\mid i,j)$ have a normalized local-hidden-state model with the same hidden ensemble at every pair of settings $i,j\in\{1,2\}$ . Alice's binary output $a$ includes a public binary detection flag $s$ , and the no-click output is predetermined. Bob's response is the Born probability of a binary rank-one projective measurement on the normalized hidden qubit state. Define $\widetilde A_i=(A_i,s_i)$ and $q=-\log_2\max_{a,b}|\langle u_{1a},u_{2b}\rangle|^2$ from Bob's two orthonormal measurement bases. Then, in bits,

H(B_1\mid\widetilde A_1)+H(B_2\mid\widetilde A_2)\ge q.

Each entropy is evaluated on its own observed same-setting marginal. Conditioning events with zero probability contribute zero. No joint distribution for incompatible Bob outcomes is required. The inequality provides a direct entropic criterion for steering.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P94

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P94

open MeasureTheory

open scoped ComplexConjugate

/-- arXiv:1109.1435v3, PDF p.6, (S5): every common normalized local-hidden-state
ensemble obeys the entropic steering inequality. Neither (S3) nor (S4) is assumed. -/
theorem entropicSteering_S5 {Lambda : Type*} [MeasurableSpace Lambda]
    (U : BobBases) (L : HiddenModel Lambda U) :
    projectiveOverlapIncompatibility U ≤ flaggedConditionalEntropy L false + flaggedConditionalEntropy L true := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P94

end

Source

One-sided Device-Independent Quantum Key Distribution: Security, feasibility, and the connection with steering, arXiv:1109.1435v3, PDF p. 6, Eq. (S5)

Read-back

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

Let $\mathbb B=\{0,1\}$ , representing false and true. For every measurable space $\Lambda$ , every pair of unitary complex matrices $U_0,U_1$ indexed by $\mathbb B$ , and every model $L$ , suppose $L$ supplies a probability measure $\mu$ , positive semidefinite trace-one matrices $\rho_\lambda$ with measurable entries, and nonnegative measurable responses $r_i(\lambda,a,s)$ satisfying $\sum_{a,s}r_i(\lambda,a,s)=1$ for every $i,\lambda$ . The model also supplies bits $c_i$ satisfying $r_i(\lambda,a,0)=0$ for $a\ne c_i$ . Define $E_{j,b}(x,y)=U_j(x,b)\overline{U_j(y,b)}$ and $q_{j,b}(\lambda)=\operatorname{Re}\operatorname{tr}(E_{j,b}\rho_\lambda)$ ; every product $r_i(\lambda,a,s)q_{j,b}(\lambda)$ must be integrable. Put $p_i(a,s,b)=\int_\Lambda r_i(\lambda,a,s)q_{i,b}(\lambda)\,d\mu(\lambda)$ , $m_i(a,s)=\sum_b p_i(a,s,b)$ , and

H_i=\sum_{a,s\in\mathbb B} \begin{cases} 0,&m_i(a,s)=0,\\ m_i(a,s)\,h_2\!\left(\dfrac{p_i(a,s,1)}{m_i(a,s)}\right),&m_i(a,s)\ne0, \end{cases} \qquad C=\max_{a,b\in\mathbb B}\left|\sum_{x\in\mathbb B}\overline{U_0(x,a)}U_1(x,b)\right|^2,

where $h_2(p)=-[p\ln p+(1-p)\ln(1-p)]/\ln2$ , with $0\ln0=0$ . Then $-\log_2 C\le H_0+H_1$ . Zero-mass pairs contribute zero, and no condition of positive detection probability or equal detection probabilities is imposed.

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