Fano inequality for the actual decoder error

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.fano

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

prove2quantum

For a finite normalized joint law p on nonempty X and Y and any decoder f:Y -> X, let e=Pr[X != f(Y)]. Then H(X|Y) <= h_2(e)+e log_2(|X|-1), with the singleton branch evaluated as 0 log 0=0. All quantities, including e and H(X|Y), are computed from p.

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, (161): decoding error is computed from the joint law and f.
For a singleton X, error and conditional entropy are zero; 0 log 0 is zero. -/
theorem fano {X Y : Type} [Fintype X] [Fintype Y] [Nonempty X] [Nonempty Y]
    (p : X × Y → ℝ) (hp : IsLaw p) (f : Y → X) :
    let err := ∑ x, ∑ y, if x = f y then 0 else p (x,y)
    shannon p - shannon (fun y => ∑ x, p (x,y)) ≤
      QAlgorithms.binEntropy2 err + err * Real.logb 2 ((Fintype.card X : ℝ) - 1) := 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 (161)

Read-back

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

For finite nonempty types $X,Y$ , a function $p:X\times Y\to\mathbb R$ with nonnegative values summing to $1$ , and any function $f:Y\to X$ , set

e=\sum_x\sum_{y:x\ne f(y)}p(x,y),\qquad p_Y(y)=\sum_xp(x,y).

Then

H(p)-H(p_Y)\le h_2(e)+e\log_2(|X|-1),

where $H(s)=-\sum_i s(i)\log_2s(i)$ and $h_2(t)=[-t\log t-(1-t)\log(1-t)]/\log2$ , with zero terms interpreted using the totalized logarithm $\log0=0$ . This includes singleton $X$ : then $e=0$ , and the displayed $\log_2(|X|-1)$ is the defined value $\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