InformationTheory.Fano

Imports 4

Fano's inequality: a mathlib-current core formalization #

Mathlib currently provides Real.binEntropy and Real.qaryEntropy. The theorem Real.qaryEntropy is exactly the textbook Fano right-hand side

binEntropy Pe + Pe * log (q - 1).

This file packages that identity as Fano's inequality, plus a monotone inverse corollary on the standard range Pe ≤ 1 - 1 / q.

For finite joint probability mass functions we also define the usual finite entropy quantities and provide a ready-to-use wrapper: once the information- theoretic core estimate

H(X | Y) ≤ Real.qaryEntropy |X| Pe

has been proved for your model, the theorem below rewrites it to the standard Fano bound.

noncomputable def

InformationTheory.fanoBoundRHS

source

(q : ℕ) (Pe : ℝ) :

ℝ

The textbook right-hand side in Fano's inequality, measured in nats.

Equations

InformationTheory.fanoBoundRHS q Pe = Real.binEntropy Pe + Pe * Real.log ↑(↑q - 1)

Instances For

Used by

theorem

InformationTheory.qaryEntropy_eq_fanoBoundRHS

source

(q : ℕ) (Pe : ℝ) :

Real.qaryEntropy q Pe = fanoBoundRHS q Pe

Real.qaryEntropy is the Fano right-hand side.

Used by

theorem

InformationTheory.fanoBoundRHS_eq_qaryEntropy

source

(q : ℕ) (Pe : ℝ) :

fanoBoundRHS q Pe = Real.qaryEntropy q Pe

The reverse rewrite, sometimes more convenient for rw.

Used by

theorem

InformationTheory.qaryEntropy_eq_binEntropy_add_log

source

(q : ℕ) (Pe : ℝ) :

Real.qaryEntropy q Pe = Real.binEntropy Pe + Pe * Real.log (↑q - 1)

qaryEntropy written as the textbook sum binEntropy Pe + Pe · log (q - 1), without going through the intermediate fanoBoundRHS definition.

Used by

theorem

InformationTheory.fano_inequality_of_le_qaryEntropy

source

{q : ℕ} {Pe Hxy : ℝ} (h : Hxy ≤ Real.qaryEntropy q Pe) :

Hxy ≤ fanoBoundRHS q Pe

Fano's inequality (q-ary form).

The hypothesis is the information-theoretic estimate Hxy ≤ qaryEntropy q Pe; the conclusion is the usual textbook display Hxy ≤ h(Pe) + Pe log(q - 1).

Used by

noncomputable def

InformationTheory.fanoBoundRHSOfAlphabet

source

(X : Type u_1) [Fintype X] (Pe : ℝ) :

ℝ

Fano's right-hand side for a finite alphabet.

Equations

InformationTheory.fanoBoundRHSOfAlphabet X Pe = InformationTheory.fanoBoundRHS (Fintype.card X) Pe

Instances For

Used by

theorem

InformationTheory.fano_inequality_of_alphabet

source

{X : Type u_1} [Fintype X] {Pe Hxy : ℝ} (h : Hxy ≤ Real.qaryEntropy (Fintype.card X) Pe) :

Hxy ≤ fanoBoundRHSOfAlphabet X Pe

Fano's inequality (finite alphabet).

Used by

theorem

InformationTheory.fano_error_lower_bound_of_lt_qaryEntropy

source

{q : ℕ} (hq : 2 ≤ q) {a Pe Hxy : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1 - 1 / ↑q) (hPe0 : 0 ≤ Pe) (hPe1 : Pe ≤ 1 - 1 / ↑q) (hFano : Hxy ≤ Real.qaryEntropy q Pe) (haH : Real.qaryEntropy q a < Hxy) :

a < Pe

Strict inverse form of the Fano bound on the increasing branch of qaryEntropy.

If a candidate lower bound a already has qaryEntropy q a < Hxy, and Fano gives Hxy ≤ qaryEntropy q Pe, then a < Pe, provided both a and Pe lie in the standard monotonicity interval [0, 1 - 1/q].

Used by

theorem

InformationTheory.fano_error_lower_bound_of_lt_fanoBoundRHS

source

{q : ℕ} (hq : 2 ≤ q) {a Pe Hxy : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1 - 1 / ↑q) (hPe0 : 0 ≤ Pe) (hPe1 : Pe ≤ 1 - 1 / ↑q) (hFano : Hxy ≤ fanoBoundRHS q Pe) (haH : fanoBoundRHS q a < Hxy) :

a < Pe

Same inverse form, but stated with the textbook Fano right-hand side.

Used by

theorem

InformationTheory.fano_error_lower_bound_of_alphabet

source

{X : Type u_1} [Fintype X] (hcard : 2 ≤ Fintype.card X) {a Pe Hxy : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1 - 1 / ↑(Fintype.card X)) (hPe0 : 0 ≤ Pe) (hPe1 : Pe ≤ 1 - 1 / ↑(Fintype.card X)) (hFano : Hxy ≤ fanoBoundRHSOfAlphabet X Pe) (haH : fanoBoundRHSOfAlphabet X a < Hxy) :

a < Pe

Alphabet-indexed inverse form of Fano's inequality.

Used by

Finite PMF interface #

structure

InformationTheory.FiniteJointPMF

source

(X : Type u_1) (Y : Type u_2) [Fintype X] [Fintype Y] :

Type (max u_1 u_2)

A finite joint probability mass function on X × Y, stored as real masses.

mass : X → Y → ℝ
mass_nonneg(x : X) (y : Y) : 0 ≤ self.mass x y
sum_mass : ∑ x : X, ∑ y : Y, self.mass x y = 1

Instances For

Used by

def

InformationTheory.FiniteJointPMF.marginalY

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (P : FiniteJointPMF X Y) (y : Y) :

ℝ

Marginal mass of Y = y.

Equations

P.marginalY y = ∑ x : X, P.mass x y

Instances For

Used by

noncomputable def

InformationTheory.FiniteJointPMF.jointEntropy

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (P : FiniteJointPMF X Y) :

ℝ

Joint Shannon entropy H(X,Y) in nats.

Equations

P.jointEntropy = ∑ x : X, ∑ y : Y, (P.mass x y).negMulLog

Instances For

Used by

noncomputable def

InformationTheory.FiniteJointPMF.yEntropy

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (P : FiniteJointPMF X Y) :

ℝ

Marginal Shannon entropy H(Y) in nats.

Equations

P.yEntropy = ∑ y : Y, (P.marginalY y).negMulLog

Instances For

Used by

noncomputable def

InformationTheory.FiniteJointPMF.condEntropy

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (P : FiniteJointPMF X Y) :

ℝ

Conditional entropy H(X | Y) = H(X,Y) - H(Y) in nats.

Equations

P.condEntropy = P.jointEntropy - P.yEntropy

Instances For

Used by

def

InformationTheory.FiniteJointPMF.errorProb

source

{X : Type u_1} [Fintype X] [DecidableEq X] (P : FiniteJointPMF X X) :

ℝ

Error probability of a Markov-form joint PMF on (X, Xh) where the second coordinate plays the role of the estimator Xh. The error event is {(x, xh) : x ≠ xh}.

Equations

P.errorProb = ∑ x : X, ∑ xh : X, if x = xh then 0 else P.mass x xh

Instances For

Used by

theorem

InformationTheory.FiniteJointPMF.fano_inequality_of_core

source

{X : Type u_1} [Fintype X] [DecidableEq X] (P : FiniteJointPMF X X) (hcore : P.condEntropy ≤ Real.qaryEntropy (Fintype.card X) P.errorProb) :

P.condEntropy ≤ fanoBoundRHSOfAlphabet X P.errorProb

Finite-PMF Fano wrapper, Markov form on (X, Xh).

After proving the model-specific core estimate P.condEntropy ≤ Real.qaryEntropy (Fintype.card X) P.errorProb, this theorem returns the standard Fano inequality.

Used by

theorem

InformationTheory.FiniteJointPMF.error_lower_bound_of_core

source

{X : Type u_1} [Fintype X] [DecidableEq X] (P : FiniteJointPMF X X) (hcard : 2 ≤ Fintype.card X) {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1 - 1 / ↑(Fintype.card X)) (hPe0 : 0 ≤ P.errorProb) (hPe1 : P.errorProb ≤ 1 - 1 / ↑(Fintype.card X)) (hcore : P.condEntropy ≤ Real.qaryEntropy (Fintype.card X) P.errorProb) (haH : Real.qaryEntropy (Fintype.card X) a < P.condEntropy) :

a < P.errorProb

Finite-PMF inverse Fano wrapper on the increasing branch, Markov form.

Used by