Pinsker inequality in bits and its mutual-information identity

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.pinsker_and_mi

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

prove2quantum

For normalized laws p,q on a finite nonempty alphabet, TV(p,q)^2 <= D_bits(p||q)/2, with support failures retained as infinity. For any normalized finite joint law r, D_bits(r||r_A r_B)=I_r(A:B). The squared inequality is equivalent to the printed square-root form because TV is nonnegative.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P22

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P22

attribute [local instance] Classical.propDecidable Classical.decEq

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

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

open QAlgorithms.Papers.Independent.Information100.P27 (shannon)

open QAlgorithms.Papers.Independent.Gap48.P25 (classicalMI)

/-- PDF p.38, (160) and the following MI identity. The displayed loose
Pinsker coefficient is in bits. Squaring preserves the inequality since TV is
nonnegative. Extended nonnegative reals retain infinity on support failure. -/
theorem pinsker_and_mi {I A B : Type}
    [Fintype I] [Fintype A] [Fintype B] [Nonempty I] [Nonempty A] [Nonempty B]
    (p q : I → ℝ) (hp : IsLaw p) (hq : IsLaw q)
    (r : A × B → ℝ) (hr : IsLaw r) :
    ENNReal.ofReal (((1/2 : ℝ) * ∑ i, |p i - q i|) ^ 2) ≤
      QAlgorithms.Papers.Independent.Renew46.P37.classicalKL p q / 2 ∧
    QAlgorithms.Papers.Independent.Renew46.P37.classicalKL r
      (fun ab => (∑ b, r (ab.1,b)) * (∑ a, r (a,ab.2))) =
      ENNReal.ofReal (classicalMI r) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P22

end

Source

Limitations on device independent key secure against non signaling adversary via the squashed non-locality, arXiv:1903.12154v7, PDF p. 38, Equation (160) and following identity

Read-back

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

For finite nonempty types $I,A,B$ , probability laws $p,q:I\to\mathbb R$ , and a probability law $r:A\times B\to\mathbb R$ , where a probability law means nonnegative values summing to $1$ , define $r_A(a)=\sum_b r(a,b)$ and $r_B(b)=\sum_a r(a,b)$ . For real functions $s,t$ on a finite type, let $D_2(s\Vert t)=+\infty$ if some $i$ satisfies $s(i)>0$ and $t(i)=0$ ; otherwise let it be the nonnegative extended-real embedding of

\sum_{i:s(i)\ne0}s(i)\log_2\!\frac{s(i)}{t(i)},

which replaces a negative result by $0$ . Then both

\operatorname{ofReal}\!\left[\left(\frac12\sum_i|p(i)-q(i)|\right)^2\right] \le \frac{D_2(p\Vert q)}2, \qquad D_2(r\Vert r_A r_B) =\operatorname{ofReal}\!\bigl(H(r_A)+H(r_B)-H(r)\bigr)

hold. Here $H(s)=-\sum_i s(i)\log_2 s(i)$ ; the mutual-information expression in the code obtains these entropies from the diagonal matrices with entries $s(i)$ , using $-\operatorname{Re}\operatorname{tr}f(\operatorname{diag}s)$ with $f(t)=t\log_2t$ . Zero-probability terms contribute $0$ , and the first inequality also includes the case $D_2(p\Vert q)=+\infty$ .

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