InformationTheory.Shannon.Han.DShearer
Han's inequality — Shearer's inequality (integer covering form) #
If S : ι → Finset (Fin n) covers each i : Fin n at least k times, then
k · H(X_{[n]}) ≤ ∑_j H(X_{S_j}).
Main statements #
shearer_inequality— the integer-covering Shearer inequality. The proof combines the subset chain rulejointEntropySubset_chain_rule, conditional-entropy monotonicitycondEntropy_subset_anti, andjointEntropySubset_univ, then swaps the double sum to expose the covering multiplicitycover i := #{j | i ∈ S j} ≥ k.
InformationTheory.Shannon.shearer_inequality
source{n : ℕ}
{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{Ω : Type u_2}
[MeasurableSpace Ω]
{ι : Type u_3}
[Fintype ι]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Fin n → Ω → α)
(hXs : ∀ (i : Fin n), Measurable (Xs i))
(S : ι → Finset (Fin n))
{k : ℕ}
(hk : ∀ (i : Fin n), k ≤ {j : ι | i ∈ S j}.card)
:
Shearer's inequality (integer covering form): if S : ι → Finset (Fin n) covers each
i : Fin n at least k times, then k · H(X_{[n]}) ≤ ∑_j H(X_{S_j}).