Skip to content

InformationTheory.Fano.CondEntropy

Imports 3

3-variable joint and conditional entropy: chain rule + deterministic collapse #

We work directly with raw mass functions μ : X → E → Y → ℝ rather than committing to a structured PMF type, because every chain rule becomes a ring identity at this level.

The two non-trivial outputs are:

the algebraic chain rules H(X, E | Y) = H(E | Y) + H(X | E, Y) and H(X, E | Y) = H(X | Y) + H(E | X, Y);
H(E | X, Y) = 0 whenever E is a deterministic function of (X, Y).

Together with entropyOfFn_le_log_supportCard and binEntropy_jensen_finset, these assemble the Fano core inequality.

Implementation notes #

This file's mass-function entropy/condEntropy are the form used by the Fano.Core development. The measure-theoretic developments (Fano.Measure, Shannon.Bridge.entropy, InformationTheory.MeasureFano.condEntropy) use a parallel formalism; the two do not depend on each other.

Marginals and joint entropies #

def

InformationTheory.Joint3.marginalY

{X : Type u_1} {E : Type u_2} {Y : Type u_3} [Fintype X] [Fintype E] (μ : X → E → Y → ℝ) (y : Y) :

Marginal mass on Y, summing out both X and E.

Equations

InformationTheory.Joint3.marginalY μ y = ∑ x : X, ∑ e : E, μ x e y

Instances For

Used by

def

InformationTheory.Joint3.marginalEY

{X : Type u_1} {E : Type u_2} {Y : Type u_3} [Fintype X] (μ : X → E → Y → ℝ) (e : E) (y : Y) :

Marginal mass on (E, Y), summing out X.

Equations

InformationTheory.Joint3.marginalEY μ e y = ∑ x : X, μ x e y

Instances For

Used by

def

InformationTheory.Joint3.marginalXY

{X : Type u_1} {E : Type u_2} {Y : Type u_3} [Fintype E] (μ : X → E → Y → ℝ) (x : X) (y : Y) :

Marginal mass on (X, Y), summing out E.

Equations

InformationTheory.Joint3.marginalXY μ x y = ∑ e : E, μ x e y

Instances For

Used by

noncomputable def

InformationTheory.Joint3.jointEntropy

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

Joint entropy H(X, E, Y).

Equations

InformationTheory.Joint3.jointEntropy μ = ∑ x : X, ∑ e : E, ∑ y : Y, (μ x e y).negMulLog

Instances For

Used by

noncomputable def

InformationTheory.Joint3.yEntropy

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

Marginal entropy H(Y).

Equations

InformationTheory.Joint3.yEntropy μ = ∑ y : Y, (InformationTheory.Joint3.marginalY μ y).negMulLog

Instances For

Used by

noncomputable def

InformationTheory.Joint3.eyEntropy

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

Marginal entropy H(E, Y).

Equations

InformationTheory.Joint3.eyEntropy μ = ∑ e : E, ∑ y : Y, (InformationTheory.Joint3.marginalEY μ e y).negMulLog

Instances For

Used by

noncomputable def

InformationTheory.Joint3.xyEntropy

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

Marginal entropy H(X, Y).

Equations

InformationTheory.Joint3.xyEntropy μ = ∑ x : X, ∑ y : Y, (InformationTheory.Joint3.marginalXY μ x y).negMulLog

Instances For

Used by

Marginal nonnegativity and Bool decomposition #

theorem

InformationTheory.Joint3.marginalEY_nonneg

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

0 ≤ marginalEY μ e y

Each (E, Y) marginal is non-negative when the joint mass is.

Used by

theorem

InformationTheory.Joint3.marginalY_nonneg

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

0 ≤ marginalY μ y

The Y marginal is non-negative when the joint mass is.

Used by

theorem

InformationTheory.Joint3.marginalY_eq_marginalEY_true_add_false

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

marginalY μ y = marginalEY μ true y + marginalEY μ false y

For a binary E = Bool, the Y marginal splits as the sum of the two (E, Y) marginals.

Used by

Conditional entropies (defined as entropy differences) #

noncomputable def

InformationTheory.Joint3.condXE_Y

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

H(X, E | Y) = H(X, E, Y) - H(Y).

Equations

InformationTheory.Joint3.condXE_Y μ = InformationTheory.Joint3.jointEntropy μ - InformationTheory.Joint3.yEntropy μ

Instances For

Used by

noncomputable def

InformationTheory.Joint3.condE_Y

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

H(E | Y) = H(E, Y) - H(Y).

Equations

InformationTheory.Joint3.condE_Y μ = InformationTheory.Joint3.eyEntropy μ - InformationTheory.Joint3.yEntropy μ

Instances For

Used by

noncomputable def

InformationTheory.Joint3.condX_EY

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

H(X | E, Y) = H(X, E, Y) - H(E, Y).

Equations

InformationTheory.Joint3.condX_EY μ = InformationTheory.Joint3.jointEntropy μ - InformationTheory.Joint3.eyEntropy μ

Instances For

Used by

noncomputable def

InformationTheory.Joint3.condX_Y

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

H(X | Y) = H(X, Y) - H(Y).

Equations

InformationTheory.Joint3.condX_Y μ = InformationTheory.Joint3.xyEntropy μ - InformationTheory.Joint3.yEntropy μ

Instances For

Used by

noncomputable def

InformationTheory.Joint3.condE_XY

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

H(E | X, Y) = H(X, E, Y) - H(X, Y).

Equations

InformationTheory.Joint3.condE_XY μ = InformationTheory.Joint3.jointEntropy μ - InformationTheory.Joint3.xyEntropy μ

Instances For

Used by

Chain rules #

theorem

InformationTheory.Joint3.chain_rule_E_first

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

condXE_Y μ = condE_Y μ + condX_EY μ

Chain rule with E first: H(X, E | Y) = H(E | Y) + H(X | E, Y).

Used by

theorem

InformationTheory.Joint3.chain_rule_X_first

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

condXE_Y μ = condX_Y μ + condE_XY μ

Chain rule with X first: H(X, E | Y) = H(X | Y) + H(E | X, Y).

Used by

Deterministic E ⇒ H(E | X, Y) = 0 #

theorem

InformationTheory.Joint3.condE_XY_zero_of_deterministic

{X : Type u_1} {E : Type u_2} {Y : Type u_3} [Fintype X] [Fintype E] [Fintype Y] [DecidableEq E] (μ : X → E → Y → ℝ) (f : X → Y → E) (hdet : ∀ (x : X) (e : E) (y : Y), μ x e y = if e = f x y then marginalXY μ x y else 0) :

condE_XY μ = 0

If E is a deterministic function of (X, Y) — formalized by saying that μ is concentrated on e = f x y and equals marginalXY μ x y there — then the conditional entropy H(E | X, Y) vanishes.

Used by