Fano's inequality: measure-theoretic form #

The measure-theoretic form of Fano's inequality (Cover–Thomas, Polyanskiy), proved with Mathlib's condDistrib (the regular conditional distribution) as the central object, for a deterministic decoder Y → X.

Setting:

• X : Fintype (discrete, finite) — the channel alphabet
• Y : MeasurableSpace (arbitrary; ℝ, ℝⁿ, Polish spaces, etc. are admissible)
• random variables Xs : Ω → X (source) and Yo : Ω → Y (observation) on (Ω, μ)
• decoder : Y → X — a deterministic measurable decoder

Main definitions #

• condEntropy μ Xs Yo — the conditional entropy H(Xs | Yo) as an integral over μ.map Yo.
• errorProb μ Xs Yo decoder — the decoding error probability P(Xs ≠ decoder ∘ Yo).

Main statements #

• fano_inequality_measure_theoretic — H(Xs | Yo) ≤ binEntropy Pe + Pe · log(|X| − 1).

Implementation notes #

The discrete Fano inequality of Fano.Core is applied pointwise for each y : Y, then aggregated into integral form on P_Yo = μ.map Yo via Bochner–Jensen. The proof chains four steps:

H(Xs | Yo)
  = ∫ y, [∑ x, negMulLog (Q_y {x})] dP_Yo                    -- def of condEntropy
  ≤ ∫ y, qaryEntropy |X| (Pe_y) dP_Yo                        -- Step 1: pointwise_fano
  ≤ qaryEntropy |X| (∫ y, Pe_y dP_Yo)                        -- Step 2: Bochner Jensen
  = qaryEntropy |X| (errorProb μ Xs Yo decoder)              -- Step 3: disintegration
  = h(Pe) + Pe · log(|X| - 1)                                -- Step 4: qaryEntropy split

Here Q_y = (condDistrib Xs Yo μ y).real is the conditional distribution of Xs given y and Pe_y = Q_y {x | x ≠ decoder y} is the error rate given y. The StandardBorelSpace requirement of condDistrib is imposed on the output type, which here is X; from Fintype + MeasurableSingletonClass + Countable the instance DiscreteMeasurableSpace → StandardBorelSpace is derived automatically, so Y carries no extra constraint.

References #

• T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.
• Y. Polyanskiy and Y. Wu, Information Theory: From Coding to Learning, Cambridge, 2024.

Definitions #

Pointwise Fano (bridge to the discrete form) #

A glue lemma for invoking the discrete Fano inequality at each y : Y, in a form with the y-dependence abstracted away: for any probability measure Q : Measure X and guess xh : X, the Shannon entropy is bounded by qaryEntropy |X| Pe. The proof applies FiniteJointPMF.fano_inequality to the FiniteJointPMF X X whose second coordinate is a Dirac mass at xh.

Computations for diracPMF #

Main theorem: Fano's inequality, measure-theoretic form #

Steps 1–4 are chained with calc. Each step is built locally as a have inside the theorem rather than as a separate lemma.