Binary conditional entropy is bounded by the entropy of the error

Proved

QAlgorithms.Papers.Independent.Intakethird100.P94.binaryConditionalEntropy_S7

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

prove2quantum

Let $A$ and $B$ be binary random variables with any normalized joint probability law. Let $Q=\Pr[A e B]$ , and let $h(t)=-t\log_2 t-(1-t)\log_2(1-t)$ , with $0\log_2 0=0$ . Then

H(B\mid A)\le h(Q).

The entropy is measured in bits, and a zero-probability conditioning event has weight zero. This bound converts observed binary disagreement probabilities into conditional-entropy upper bounds for the steering inequalities.

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, (S7): for every normalized joint binary law,
H(B|A) <= h(Pr[A != B]), including zero-mass conditioning events. -/
theorem binaryConditionalEntropy_S7 (P : Bool → Bool → ℝ)
    (hNonneg : ∀ a b, 0 ≤ P a b)
    (hTotal : ∑ a : Bool, ∑ b : Bool, P a b = 1) :
    conditionalEntropyBits P ≤ QAlgorithms.binEntropy2 (binaryError P) := 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. (S7)

Read-back

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

For every real-valued array $P(a,b)$ , indexed by $a,b\in\mathbb B=\{0,1\}$ , assume that $P(a,b)\ge0$ for every pair and that $\sum_{a,b}P(a,b)=1$ . Put $m_a=\sum_bP(a,b)$ , let $e=\sum_{a\ne b}P(a,b)=P(0,1)+P(1,0)$ , and define $h_2(p)=-[p\ln p+(1-p)\ln(1-p)]/\ln2$ , with $0\ln0=0$ . Then

\sum_{a\in\mathbb B} \begin{cases} 0,&m_a=0,\\ m_a\,h_2\!\left(\dfrac{P(a,1)}{m_a}\right),&m_a\ne0 \end{cases} \ \le\ h_2(e).

The assumptions allow zero rows and error probabilities $e=0$ or $e=1$ ; zero rows contribute zero.

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