InformationTheory.Shannon.Han.Basic
Joint entropy on Fin n, the n-variable chain rule, and Han's inequality #
The Shannon joint entropy of a finite family of random variables, its n-variable chain
rule (obtained by iterating the two-variable rule
entropy_pair_eq_entropy_add_condEntropy along prefixes of Fin n), and Han's inequality.
Main definitions #
jointEntropy μ Xs— the joint entropy ofXs : Fin n → Ω → α.jointEntropyExcept μ Xs i— the joint entropy of the family with coordinateiremoved.
Main statements #
jointEntropy_chain_rule—H(X₀, …, X_{n-1}) = ∑ i, H(Xᵢ | X₀, …, X_{i-1}).han_inequality—(n − 1) · H(Xs) ≤ ∑ i, H(Xs except i).
InformationTheory.Shannon.jointEntropy
source{n : ℕ}
{α : Type u_1}
[Fintype α]
[MeasurableSpace α]
{Ω : Type u_2}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
(Xs : Fin n → Ω → α)
:
Joint entropy of a finite family of random variables.
Equations
- InformationTheory.Shannon.jointEntropy μ Xs = InformationTheory.Shannon.entropy μ fun (ω : Ω) (i : Fin n) => Xs i ω
Instances For
Used by
InformationTheory.Shannon.jointEntropyExcept
source{n : ℕ}
{α : Type u_1}
[Fintype α]
[MeasurableSpace α]
{Ω : Type u_2}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
(Xs : Fin n → Ω → α)
(i : Fin n)
:
Joint entropy with the i-th coordinate removed.
Equations
- InformationTheory.Shannon.jointEntropyExcept μ Xs i = InformationTheory.Shannon.entropy μ fun (ω : Ω) (j : { j : Fin n // j ≠ i }) => Xs (↑j) ω
Instances For
Used by
InformationTheory.Shannon.jointEntropy_chain_rule
source{n : ℕ}
{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{Ω : Type u_2}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Fin n → Ω → α)
(hXs : ∀ (i : Fin n), Measurable (Xs i))
:
jointEntropy μ Xs = ∑ i : Fin n, MeasureFano.condEntropy μ (Xs i) fun (ω : Ω) (j : Fin ↑i) => Xs ⟨↑j, ⋯⟩ ω
The n-variable chain rule for Shannon joint entropy:
H(X₀, …, X_{n-1}) = ∑ i, H(Xᵢ | X₀, …, X_{i-1}).
Used by
Han's inequality #
InformationTheory.Shannon.han_inequality
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{Ω : Type u_2}
[MeasurableSpace Ω]
{n : ℕ}
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Fin n → Ω → α)
(hXs : ∀ (i : Fin n), Measurable (Xs i))
:
Han's inequality: for a finite family Xs : Fin n → Ω → α of random variables,
(n − 1) · H(Xs) ≤ ∑ i, H(Xs except i). The degenerate cases n = 0, 1 (both sides 0)
are included.