InformationTheory.Shannon.Han.D
Han's inequality — subset joint entropy #
Joint entropy H(X_S) over an arbitrary subset S : Finset (Fin n) of coordinates, with
the subset chain rule, conditioning monotonicity, and the subset form of Han's inequality.
Main definitions #
jointEntropySubset μ Xs S— the joint entropy of the(i : ↑S) → α-valued family.
Main statements #
jointEntropySubset_univ— agrees withjointEntropy μ XswhenS = univ.jointEntropySubset_chain_rule— the subset chain ruleH(X_S) = ∑ i ∈ S, H(Xᵢ | X_{S ∩ {j < i}}).condEntropy_subset_anti— conditioning monotonicity:T₁ ⊆ T₂makes the conditional entropy smaller.han_inequality_subset— the subset form(|S| − 1) · H(X_S) ≤ ∑ i ∈ S, H(X_{S \ {i}}).
InformationTheory.Shannon.jointEntropySubset
source{n : ℕ}
{α : Type u_1}
[Fintype α]
[MeasurableSpace α]
{Ω : Type u_2}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
(Xs : Fin n → Ω → α)
(S : Finset (Fin n))
:
The joint entropy over a subset S : Finset (Fin n), i.e. the entropy of the
(i : ↑S) → α-valued random variable.
Equations
- InformationTheory.Shannon.jointEntropySubset μ Xs S = InformationTheory.Shannon.entropy μ fun (ω : Ω) (i : ↥S) => Xs (↑i) ω
Instances For
Used by
InformationTheory.Shannon.jointEntropySubset_univ
source{n : ℕ}
{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{Ω : Type u_2}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
(Xs : Fin n → Ω → α)
(hXs : ∀ (i : Fin n), Measurable (Xs i))
:
For S = Finset.univ, the subset joint entropy agrees with jointEntropy μ Xs.
Used by
InformationTheory.Shannon.jointEntropySubset_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))
(S : Finset (Fin n))
:
jointEntropySubset μ Xs S = ∑ i ∈ S, MeasureFano.condEntropy μ (Xs i) fun (ω : Ω) (j : ↥({x ∈ S | x < i})) => Xs (↑j) ω
The subset chain rule: H(X_S) = ∑ i ∈ S, H(Xᵢ | X_{S ∩ {j < i}}).
Used by
InformationTheory.Shannon.condEntropy_subset_anti
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))
(i : Fin n)
{T₁ T₂ : Finset (Fin n)}
(hT : T₁ ⊆ T₂)
:
(MeasureFano.condEntropy μ (Xs i) fun (ω : Ω) (j : ↥T₂) => Xs (↑j) ω) ≤ MeasureFano.condEntropy μ (Xs i) fun (ω : Ω) (j : ↥T₁) => Xs (↑j) ω
Conditioning monotonicity on subsets: T₁ ⊆ T₂ implies
H(Xᵢ | X_{T₂}) ≤ H(Xᵢ | X_{T₁}).
Used by
InformationTheory.Shannon.han_inequality_subset
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))
(S : Finset (Fin n))
:
Han's inequality (subset form):
(|S| − 1) · H(X_S) ≤ ∑ i ∈ S, H(X_{S \ {i}}).