InformationTheory.Shannon.Polymatroid

Imports 4

Polymatroid axioms for joint entropy #

jointEntropySubset (from Han/D.lean) satisfies the three polymatroid rank function axioms:

jointEntropySubset_empty — H(X_∅) = 0.
jointEntropySubset_mono — S ⊆ T ⟹ H(X_S) ≤ H(X_T).
jointEntropySubset_submodular — H(X_{S∪T}) + H(X_{S∩T}) ≤ H(X_S) + H(X_T).

Main statements #

jointEntropySubset_empty, jointEntropySubset_mono, jointEntropySubset_submodular — the three polymatroid axioms.
entropyPolymatroid — joint entropy as a Combinatorics.Polymatroid term.

Implementation notes #

Monotonicity uses MeasurableEquiv.piFinsetUnion to reshape T = S ⊔ (T\S) as a pair, then applies the pair chain rule and condEntropy ≥ 0. Submodularity uses the three-piece disjoint decomposition S ∪ T = I ⊔ A ⊔ B (I := S∩T, A := S\T, B := T\S) and condEntropy_le_condEntropy_of_pair.

Empty subset entropy #

theorem

InformationTheory.Shannon.jointEntropySubset_empty

source

{n : ℕ} {α : Type u_1} [Fintype α] [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) :

jointEntropySubset μ Xs ∅ = 0

Polymatroid axiom (i): empty subset entropy is zero.

(↥(∅ : Finset (Fin n)) → α) is Unique via Pi.uniqueOfIsEmpty, so the push-forward measure is concentrated on default and Real.negMulLog 1 = 0.

Used by

Monotonicity #

theorem

InformationTheory.Shannon.jointEntropySubset_mono

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 T : Finset (Fin n)} (h : S ⊆ T) :

jointEntropySubset μ Xs S ≤ jointEntropySubset μ Xs T

Polymatroid axiom (ii): monotonicity in S.

T = S ⊔ (T \ S) reshape via MeasurableEquiv.piFinsetUnion followed by the pair chain rule and condEntropy ≥ 0.

Used by

Subset chain rule helper #

A "disjoint union" version of the pair chain rule that lets the caller specify the target U directly (avoiding T₂ \ T₁ casts).

theorem

InformationTheory.Shannon.jointEntropySubset_disjoint_union

source

jointEntropySubset μ Xs U = jointEntropySubset μ Xs s + MeasureFano.condEntropy μ (fun (ω : Ω) (j : ↥t) => Xs (↑j) ω) fun (ω : Ω) (j : ↥s) => Xs (↑j) ω

Disjoint-union pair chain rule. If s ∪ t = U and Disjoint s t, then H(X_U) = H(X_s) + H(X_t | X_s).

Proof: build e : ((↥s → α) × (↥t → α)) ≃ᵐ (↥U → α) directly from subsetSplitMEquivAux (Mathlib MeasurableEquiv.piFinsetUnion + cast), then apply the pair chain rule.

Used by

theorem

InformationTheory.Shannon.condEntropy_reshape_disjoint_union

source

{n : ℕ} {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (Xc : Ω → β) (hXc : Measurable Xc) {s t U : Finset (Fin n)} (hd : Disjoint s t) (hU : s ∪ t = U) :

(MeasureFano.condEntropy μ Xc fun (ω : Ω) (j : ↥U) => Xs (↑j) ω) = MeasureFano.condEntropy μ Xc fun (ω : Ω) => (fun (j : ↥s) => Xs (↑j) ω, fun (j : ↥t) => Xs (↑j) ω)

condEntropy reshape under disjoint union: when Disjoint s t and s ∪ t = U, the condEntropy with conditioner X_U equals the condEntropy with conditioner the pair (X_s, X_t).

Used by

Submodularity #

theorem

InformationTheory.Shannon.jointEntropySubset_submodular

source

jointEntropySubset μ Xs (S ∪ T) + jointEntropySubset μ Xs (S ∩ T) ≤ jointEntropySubset μ Xs S + jointEntropySubset μ Xs T

Polymatroid axiom (iii): submodularity.

3-piece disjoint decomposition S ∪ T = I ⊔ A ⊔ B with I := S ∩ T, A := S \ T, B := T \ S. Expand each side via chain rule and apply condEntropy_le_condEntropy_of_pair once.

Used by

Polymatroid wrapper #

Joint entropy as a Combinatorics.Polymatroid term: the four polymatroid axioms are exactly the three theorems above (jointEntropySubset_empty / jointEntropySubset_mono / jointEntropySubset_submodular), repackaged into the Polymatroid structure introduced in InformationTheory/Polymatroid/Basic.lean.

noncomputable def

InformationTheory.Shannon.entropyPolymatroid

source

Combinatorics.Polymatroid (Fin n)

Joint entropy as a polymatroid rank function.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by