Skip to content

InformationTheory.Fano.Core

Imports 7

Fano core proof: error indicator + chain-rule glue (Markov form) #

Markov-form variant of the Fano core: the joint PMF lives on (X, Xh) where both coordinates take values in the same finite alphabet X, and the error event is {(x, xh) : x ≠ xh} rather than {(x, y) : x ≠ decode y}. The deterministic-decoder form decode : Y → X is recovered downstream via the data processing inequality.

errIndicator : X → X → Bool — decide (x ≠ xh).
withErr P : X → Bool → X → ℝ — the 3-variable mass extending a finite joint PMF on (X, Xh) with the deterministic indicator coordinate.
Bridge lemmas connecting withErr's Joint3.* quantities to the original FiniteJointPMF ones, plus the specialization withErr_condE_XY_zero of M2's deterministic-collapse lemma.
withErr_marginalEY_true_sum recovers the error probability from the (E, Xh) marginal at E = true.

Joint3-level rearrangement for binary `E` #

H(E | Y) of a 3-variable mass with E = Bool collapses to a weighted sum of binEntropy over Y, where the weights are the Y marginal and the points are the conditional probabilities P(E = 1 | Y = y).

theorem

InformationTheory.Joint3.condE_Y_eq_sum_marginalY_mul_binEntropy

{X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (μ : X → Bool → Y → ℝ) (h_nn : ∀ (x : X) (e : Bool) (y : Y), 0 ≤ μ x e y) :

condE_Y μ = ∑ y : Y, marginalY μ y * Real.binEntropy (marginalEY μ true y / marginalY μ y)

Used by

theorem

InformationTheory.Joint3.condX_EY_eq_sum_per_ey

{X : Type u_3} {E : Type u_4} {Y : Type u_5} [Fintype X] [Fintype E] [Fintype Y] (μ : X → E → Y → ℝ) :

condX_EY μ = ∑ e : E, ∑ y : Y, (∑ x : X, (μ x e y).negMulLog - (marginalEY μ e y).negMulLog)

Per-(e, y) decomposition of condX_EY:

H(X | E, Y) = ∑ e, ∑ y, [(∑ x, negMulLog μ(x, e, y)) - negMulLog (marginalEY μ e y)].

Used by

Non-normalized maximum-entropy bound #

(∑ a, negMulLog μ a) - negMulLog (∑ a, μ a) ≤ (∑ a, μ a) * log |S| whenever the support of μ is contained in a Finset S.

theorem

InformationTheory.sum_negMulLog_sub_le_sum_mul_log_card

{α : Type u_1} [Fintype α] (μ : α → ℝ) (h_nn : ∀ (a : α), 0 ≤ μ a) {S : Finset α} (h_supp : ∀ a ∉ S, μ a = 0) :

∑ a : α, (μ a).negMulLog - (∑ a : α, μ a).negMulLog ≤ (∑ a : α, μ a) * Real.log ↑S.card

Used by

def

InformationTheory.FiniteJointPMF.errIndicator

{X : Type u_1} [DecidableEq X] :

X → X → Bool

Decoding-error indicator (Markov form): errIndicator x xh = true iff the estimator xh differs from the source x.

Equations

InformationTheory.FiniteJointPMF.errIndicator x xh = decide (x ≠ xh)

Instances For

Used by

def

InformationTheory.FiniteJointPMF.withErr

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

X → Bool → X → ℝ

The 3-variable mass extending P with the decoding-error coordinate.

The point (x, e, xh) carries mass P.mass x xh exactly when e agrees with errIndicator x xh, and 0 otherwise.

Equations

P.withErr x e xh = if e = InformationTheory.FiniteJointPMF.errIndicator x xh then P.mass x xh else 0

Instances For

Used by

Bridge to `Joint3` quantities #

theorem

InformationTheory.FiniteJointPMF.withErr_marginalXY

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

Joint3.marginalXY P.withErr x xh = P.mass x xh

The (X, Xh) marginal of withErr recovers the original 2-variable mass.

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_marginalY

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

Joint3.marginalY P.withErr xh = P.marginalY xh

The Xh marginal of withErr agrees with the original marginalY.

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_xyEntropy

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

Joint3.xyEntropy P.withErr = P.jointEntropy

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_yEntropy

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

Joint3.yEntropy P.withErr = P.yEntropy

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_condX_Y

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

Joint3.condX_Y P.withErr = P.condEntropy

H(X | Xh) for the original PMF agrees with Joint3.condX_Y of the 3-variable extension.

Used by

`withErr` is deterministic in the `E` coordinate #

theorem

InformationTheory.FiniteJointPMF.withErr_isDeterministic

{X : Type u_1} [Fintype X] [DecidableEq X] (P : FiniteJointPMF X X) (x : X) (e : Bool) (xh : X) :

P.withErr x e xh = if e = errIndicator x xh then Joint3.marginalXY P.withErr x xh else 0

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_condE_XY_zero

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

Joint3.condE_XY P.withErr = 0

H(E | X, Xh) = 0 for the deterministic indicator extension.

Used by

Marginal of `E = true` equals the error probability #

theorem

InformationTheory.FiniteJointPMF.withErr_marginalEY_true_sum

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

∑ xh : X, Joint3.marginalEY P.withErr true xh = P.errorProb

Used by

M5(2): `H(E | Xh) ≤ binEntropy Pe` #

theorem

InformationTheory.FiniteJointPMF.withErr_nonneg

{X : Type u_1} [Fintype X] [DecidableEq X] (P : FiniteJointPMF X X) (x : X) (e : Bool) (xh : X) :

0 ≤ P.withErr x e xh

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_marginalY_sum

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

∑ xh : X, Joint3.marginalY P.withErr xh = 1

The Xh-marginal sum on withErr equals 1 (since P is a PMF).

Used by

theorem

InformationTheory.FiniteJointPMF.withErr_condE_Y_le_binEntropy_errorProb

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

Joint3.condE_Y P.withErr ≤ Real.binEntropy P.errorProb

The conditional entropy H(E | Xh) of the indicator extension is bounded above by binEntropy of the estimator's error probability.

Used by

M5(3): `H(X | E, Xh) ≤ Pe * log(|X| - 1)` #

theorem

InformationTheory.FiniteJointPMF.withErr_condX_EY_le

{X : Type u_1} [Fintype X] [DecidableEq X] (P : FiniteJointPMF X X) (hcard : 1 ≤ Fintype.card X) :

Joint3.condX_EY P.withErr ≤ P.errorProb * Real.log (↑(Fintype.card X) - 1)

The conditional entropy H(X | E, Xh) of the indicator extension is bounded above by Pe * log(|X| - 1).

Used by

M6: assembled Fano core inequality #

theorem

InformationTheory.FiniteJointPMF.fano_core

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

P.condEntropy ≤ Real.qaryEntropy (Fintype.card X) P.errorProb

Fano's inequality (core, Markov form): H(X | Xh) ≤ qaryEntropy |X| P.errorProb.

Used by

theorem

InformationTheory.FiniteJointPMF.errorProb_nonneg

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

0 ≤ P.errorProb

The error probability is non-negative.

Used by

theorem

InformationTheory.FiniteJointPMF.fano_inequality

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

P.condEntropy ≤ fanoBoundRHSOfAlphabet X P.errorProb

Fano's inequality (Markov form, textbook RHS): H(X | Xh) ≤ binEntropy Pe + Pe · log(|X| - 1), with no external hcore hypothesis.

Used by

theorem

InformationTheory.FiniteJointPMF.error_lower_bound

{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)) (hPe1 : P.errorProb ≤ 1 - 1 / ↑(Fintype.card X)) (haH : Real.qaryEntropy (Fintype.card X) a < P.condEntropy) :

a < P.errorProb

Strict inverse form of Fano's inequality on the increasing branch (Markov form), with no external hcore hypothesis (and errorProb non-negativity absorbed into the proof).

Used by