InformationTheory.Fano.DPI

Imports 9

Data processing inequality (deterministic post-processing) #

For a finite joint PMF P : FiniteJointPMF X Y and a deterministic "decoder" f : Y → X, the pushforward P.pushforward f : FiniteJointPMF X X has conditional entropy at least as large as the original:

P.condEntropy ≤ (P.pushforward f).condEntropy, i.e. H(X | Y) ≤ H(X | f(Y)).

This is the deterministic-post-processing case of the data processing inequality. The proof goes through the log-sum inequality (Jensen on Real.negMulLog) applied per fiber f⁻¹{xh}.

The decoder form decode : Y → X of Fano's inequality is recovered downstream by combining DPI with the Markov-form fano_inequality.

Log-sum inequality (negMulLog form) #

theorem

InformationTheory.log_sum_inequality_negMulLog

source

{ι : Type u_1} (s : Finset ι) (a b : ι → ℝ) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (h_ac : ∀ i ∈ s, b i = 0 → a i = 0) :

∑ i ∈ s, ((a i).negMulLog + a i * Real.log (b i)) ≤ (∑ i ∈ s, a i).negMulLog + (∑ i ∈ s, a i) * Real.log (∑ i ∈ s, b i)

Log-sum inequality, negMulLog form. For finite ι, nonneg a, b : ι → ℝ with the absolute-continuity condition b i = 0 → a i = 0,

∑ (negMulLog (a i) + a i * log (b i)) ≤ negMulLog (∑ a i) + (∑ a i) * log (∑ b i).

This is Jensen's inequality on the concave function negMulLog.

Used by

Pushforward of a finite joint PMF #

def

InformationTheory.FiniteJointPMF.pushforward

source

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

FiniteJointPMF X X

Pushforward of a finite joint PMF under a deterministic function f : Y → Xh. The new joint PMF on (X, Xh) has mass given by summing over the fiber f⁻¹{xh}.

Equations

P.pushforward f = { mass := fun (x xh : X) => ∑ y : Y with f y = xh, P.mass x y, mass_nonneg := ⋯, sum_mass := ⋯ }

Instances For

Used by

theorem

InformationTheory.FiniteJointPMF.pushforward_marginalY

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] [DecidableEq X] (P : FiniteJointPMF X Y) (f : Y → X) (xh : X) :

(P.pushforward f).marginalY xh = ∑ y : Y with f y = xh, P.marginalY y

Marginal of the pushforward: (P.pushforward f).marginalY xh = ∑_{y : f y = xh} P.marginalY y.

Used by

DPI: H(X | Y) ≤ H(X | f(Y)) #

theorem

InformationTheory.FiniteJointPMF.condEntropy_le_pushforward_condEntropy

source

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

P.condEntropy ≤ (P.pushforward f).condEntropy

Data processing inequality (deterministic post-processing): the conditional entropy of X given Y does not exceed the conditional entropy of X given f(Y).

Used by

Compatibility of the Markov-form errorProb with the decoder form #

theorem

InformationTheory.FiniteJointPMF.pushforward_errorProb

source

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

(P.pushforward f).errorProb = ∑ x : X, ∑ y : Y, if x = f y then 0 else P.mass x y

The Markov-form error probability of a pushforward agrees with the decoder error probability.

Used by

Decoder form recovered from Markov Fano + DPI #

theorem

InformationTheory.FiniteJointPMF.fano_inequality_decode

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] [DecidableEq X] (P : FiniteJointPMF X Y) (decode : Y → X) (hcard : 2 ≤ Fintype.card X) :

P.condEntropy ≤ fanoBoundRHSOfAlphabet X (P.pushforward decode).errorProb

Fano's inequality (decoder form): for a deterministic decoder decode : Y → X,

H(X | Y) ≤ binEntropy Pe + Pe * log (|X| - 1)

with Pe = ∑ {(x, y) : x ≠ decode y}, P.mass x y.

See also fano_inequality, condEntropy_le_pushforward_condEntropy.

Used by

theorem

InformationTheory.FiniteJointPMF.fano_inequality_decode'

source

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] [DecidableEq X] (P : FiniteJointPMF X Y) (decode : Y → X) (hcard : 2 ≤ Fintype.card X) :

P.condEntropy ≤ fanoBoundRHSOfAlphabet X (∑ x : X, ∑ y : Y, if x = decode y then 0 else P.mass x y)

Decoder form of Fano's inequality, with the error probability written in the explicit double-sum form ∑ x, ∑ y, if x = decode y then 0 else P.mass x y.

Used by

theorem

InformationTheory.FiniteJointPMF.error_lower_bound_decode

source

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

a < (P.pushforward decode).errorProb

Decoder form of the strict inverse Fano bound (error_lower_bound) for a deterministic decoder.

Used by