InformationTheory.Shannon.LoomisWhitney

Imports 4

Loomis–Whitney inequality (information-theoretic proof) #

For any finite alphabet α and non-empty finite set A : Finset (Fin n → α): $| A |^{n - 1} \leq \prod_{i : Fin n} | π_{i} (A) |,$ where π_i(A) is the projection of A onto all coordinates except i.

Main definitions #

projectionExcept i A — projection of A : Finset (Fin n → α) onto {j : Fin n // j ≠ i}.

Main statements #

entropy_uniformOn_eq_log_card — entropy (uniformOn A) id = log #A.
entropy_le_log_image_card — entropy (uniformOn A) f ≤ log #(A.image f).
loomis_whitney — the Loomis–Whitney inequality.

Implementation notes #

The proof takes μ := uniformOn (A : Set (Fin n → α)) and Xs i ω := ω i, applies shearer_inequality with cover S i := univ.filter (· ≠ i) (each coordinate covered n - 1 times), bounds each marginal entropy by log #(projectionExcept i A) via Jensen / entropy_le_log_image_card, and converts ∑ log = log ∏ to peel off the logarithm.

Entropy on counting measures #

theorem

InformationTheory.Shannon.entropy_uniformOn_eq_log_card

source

{β : Type u_1} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {A : Finset β} (hA : A.Nonempty) :

entropy (ProbabilityTheory.uniformOn ↑A) id = Real.log ↑A.card

The entropy of the identity on the uniform distribution over A equals log #A.

Used by

theorem

InformationTheory.Shannon.entropy_le_log_image_card

source

{β : Type u_1} {γ : Type u_2} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] {A : Finset β} (hA : A.Nonempty) (f : β → γ) (hf : Measurable f) :

entropy (ProbabilityTheory.uniformOn ↑A) f ≤ Real.log ↑(Finset.image f A).card

For μ = uniformOn (A : Set β), entropy μ f ≤ log #(A.image f).

Proof: apply Jensen's inequality for negMulLog (concave on [0, ∞)) to bound ∑ negMulLog p_y ≤ N · negMulLog (1/N), then use negMulLog (1/N) = (log N)/N.

Used by

Coordinate projections #

def

InformationTheory.Shannon.projectionExcept

source

{n : ℕ} {α : Type u_1} [DecidableEq α] (i : Fin n) (A : Finset (Fin n → α)) :

Finset ({ j : Fin n // j ≠ i } → α)

Projection of A : Finset (Fin n → α) onto coordinates except i.

Equations

InformationTheory.Shannon.projectionExcept i A = Finset.image (fun (x : Fin n → α) (j : { j : Fin n // j ≠ i }) => x ↑j) A

Instances For

Used by

theorem

InformationTheory.Shannon.jointEntropySubset_le_log_projectionExcept_card

source

{n : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {A : Finset (Fin n → α)} (hA : A.Nonempty) (i : Fin n) :

jointEntropySubset (ProbabilityTheory.uniformOn ↑A) (fun (i : Fin n) (ω : Fin n → α) => ω i) {j : Fin n | j ≠ i} ≤ Real.log ↑(projectionExcept i A).card

Used by

Loomis–Whitney main theorem #

theorem

InformationTheory.Shannon.loomis_whitney

source

{n : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {A : Finset (Fin n → α)} (hA : A.Nonempty) :

A.card ^ (n - 1) ≤ ∏ i : Fin n, (projectionExcept i A).card

The Loomis–Whitney inequality (information-theoretic proof).

For any non-empty A : Finset (Fin n → α), A.card ^ (n - 1) ≤ ∏ i : Fin n, (projectionExcept i A).card.

Used by