Finite Shannon entropy

Entropy is measured in bits. Conditional entropy is the joint entropy minus the entropy of the observed first component. For a joint distribution presented as a marginal and a conditional kernel, this is exactly the average entropy of the kernel. Both descriptions use ordinary PMFs.

The deterministic chain rule accounts for all the entropy of a source after exposing a function and then a predicate. This is the entropy accounting used in the OWF-to-PRG construction; an entropy identity alone makes no claim about computational indistinguishability.

Main definitions

• Cslib.Probability.PMF.surprisal: information content of a supported outcome in bits.
• Cslib.Probability.PMF.entropy: finite Shannon entropy.
• Cslib.Probability.PMF.conditionalEntropy: remaining entropy after an observation.

Main results

• Cslib.Probability.PMF.entropy_bind_pair, .entropy_bind_sigma: joint entropy decompositions.
• Cslib.Probability.PMF.conditionalEntropy_eq_sum: average of conditional entropies.
• Cslib.Probability.PMF.conditionalEntropy_map_fst_ge: forgetting observations increases entropy.
• Cslib.Probability.PMF.entropy_chain_rule_deterministic: deterministic chain rule.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Sections 3.3 and 5. Section 5 uses H(g(W)) + H(P(W) | g(W)) + H(W | g(W), P(W)) = H(W) to count output bits.

Adapted from Probability/Entropy.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared PMF and conditioning APIs.

noncomputable def Cslib.Probability.PMF.surprisal {α : Type u_1} (p : PMF α) (a : α) : ℝ

Information content of an outcome, in bits. For finite entropy sums we assign zero at null outcomes, which are never sampled. Identities requiring positive mass explicitly require support membership.

theorem Cslib.Probability.PMF.surprisal_nonneg {α : Type u_1} (p : PMF α) (a : α) : 0 ≤ surprisal p a

Information content is nonnegative, including the chosen value at null outcomes.

theorem Cslib.Probability.PMF.surprisal_le_of_mass_ge {α : Type u_1} (p : PMF α) (a : α) {bound : ℝ} (hmass : 2 ^ (-bound) ≤ (p a).toReal) : surprisal p a ≤ bound

A lower bound on the outcome's probability bounds its information content.

theorem Cslib.Probability.PMF.surprisal_le_iff_mass_ge {α : Type u_1} (p : PMF α) (a : α) (ha : a ∈ p.support) {bound : ℝ} : surprisal p a ≤ bound ↔ 2 ^ (-bound) ≤ (p a).toReal

On the support, an upper information bound is exactly a lower probability bound.

noncomputable def Cslib.Probability.PMF.entropy {α : Type u_1} [Finite α] (p : PMF α) : ℝ

Shannon entropy of a finite distribution, in bits. Zero masses contribute zero.

theorem Cslib.Probability.PMF.entropy_eq_sum {α : Type u_1} [Fintype α] (p : PMF α) : entropy p = (∑ a : α, (p a).toReal.negMulLog) / Real.log 2

The finite sum formula does not depend on the choice of enumeration.

theorem Cslib.Probability.PMF.entropy_eq_sum_surprisal {α : Type u_1} [Fintype α] (p : PMF α) : entropy p = ∑ a : α, (p a).toReal * surprisal p a

Entropy is the expected information content -log₂ p(a).

theorem Cslib.Probability.PMF.entropy_nonneg {α : Type u_1} [Finite α] (p : PMF α) : 0 ≤ entropy p

Finite entropy is nonnegative.

@[simp]

theorem Cslib.Probability.PMF.entropy_pure {α : Type u_1} [Finite α] (a : α) : entropy (PMF.pure a) = 0

A deterministic value carries no entropy.

theorem Cslib.Probability.PMF.entropy_eq_zero_of_subsingleton_support {α : Type u_1} [Finite α] (p : PMF α) (h : p.support.Subsingleton) : entropy p = 0

A distribution supported on at most one value carries no entropy.

@[simp]

theorem Cslib.Probability.PMF.entropy_uniform {α : Type u_1} [Fintype α] [Nonempty α] : entropy (uniformOfFintype α) = Real.logb 2 ↑(Fintype.card α)

A uniform sample has the logarithm of its cardinality as entropy.

theorem Cslib.Probability.PMF.entropy_le_log_card {α : Type u_1} [Fintype α] (p : PMF α) : entropy p ≤ Real.logb 2 ↑(Fintype.card α)

Uniform sampling maximizes entropy on a fixed finite type.

theorem Cslib.Probability.PMF.entropy_map_eq_sum {α : Type u_1} {β : Type u_2} [Fintype α] [Finite β] (p : PMF α) (f : α → β) : entropy (PMF.map f p) = ∑ a : α, (p a).toReal * surprisal (PMF.map f p) (f a)

Entropy of a deterministic observation, averaged over its original source.

theorem Cslib.Probability.PMF.entropy_map_le {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (p : PMF α) (f : α → β) : entropy (PMF.map f p) ≤ entropy p

A deterministic observation cannot increase entropy.

theorem Cslib.Probability.PMF.entropy_map_of_injOn {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (p : PMF α) {f : α → β} (hf : Set.InjOn f p.support) : entropy (PMF.map f p) = entropy p

Re-encoding preserves entropy when distinct supported outcomes remain distinct.

theorem Cslib.Probability.PMF.entropy_map_of_injective {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (p : PMF α) {f : α → β} (hf : Function.Injective f) : entropy (PMF.map f p) = entropy p

Injective re-encoding preserves entropy.

theorem Cslib.Probability.PMF.sum_mul_entropy_le_entropy_bind {α : Type u_1} {β : Type u_2} [Fintype α] [Finite β] (p : PMF α) (kernel : α → PMF β) : ∑ a : α, (p a).toReal * entropy (kernel a) ≤ entropy (p.bind kernel)

Mixing finite distributions cannot lower their average entropy.

theorem Cslib.Probability.PMF.entropy_bind_pair {α : Type u_1} {β : Type u_2} [Fintype α] [Finite β] (p : PMF α) (kernel : α → PMF β) : entropy (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (kernel a)) = entropy p + ∑ a : α, (p a).toReal * entropy (kernel a)

The joint entropy is the marginal entropy plus the average conditional entropy.

theorem Cslib.Probability.PMF.entropy_bind_sigma {α : Type u_1} {β : α → Type u_4} [Fintype α] [∀ (a : α), Finite (β a)] (p : PMF α) (kernel : (a : α) → PMF (β a)) : entropy (p.bind fun (a : α) => PMF.map (Sigma.mk a) (kernel a)) = entropy p + ∑ a : α, (p a).toReal * entropy (kernel a)

Entropy also decomposes when the second sample's alphabet depends on the first.

theorem Cslib.Probability.PMF.entropy_prod {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (p : PMF α) (q : PMF β) : entropy (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) q) = entropy p + entropy q

Independent sources add their entropies.

noncomputable def Cslib.Probability.PMF.conditionalEntropy {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (joint : PMF (α × β)) : ℝ

Entropy of the second component given the first, in bits.

theorem Cslib.Probability.PMF.conditionalEntropy_nonneg {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (joint : PMF (α × β)) : 0 ≤ conditionalEntropy joint

Conditioning leaves nonnegative entropy.

@[simp]

theorem Cslib.Probability.PMF.conditionalEntropy_map_const {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (p : PMF β) (a : α) : conditionalEntropy (PMF.map (fun (x : β) => (a, x)) p) = entropy p

A constant observation reveals nothing about the sampled value.

theorem Cslib.Probability.PMF.conditionalEntropy_bind_pair {α : Type u_1} {β : Type u_2} [Fintype α] [Finite β] (p : PMF α) (kernel : α → PMF β) : conditionalEntropy (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (kernel a)) = ∑ a : α, (p a).toReal * entropy (kernel a)

The difference-of-entropies definition equals the usual average of conditional entropies.

theorem Cslib.Probability.PMF.conditionalEntropy_bind_sigma {α : Type u_1} {γ : Type u_3} {β : α → Type u_4} [Fintype α] [∀ (a : α), Finite (β a)] [Finite γ] (p : PMF α) (kernel : (a : α) → PMF (β a × γ)) : conditionalEntropy (p.bind fun (a : α) => PMF.map (fun (pair : β a × γ) => (⟨a, pair.1⟩, pair.2)) (kernel a)) = ∑ a : α, (p a).toReal * conditionalEntropy (kernel a)

When a branch index is public, its remaining conditional entropy is the average over branches. The observed alphabet may depend on the index, as with variable-length hashes.

theorem Cslib.Probability.PMF.conditionalEntropy_eq_sum {α : Type u_1} {β : Type u_2} [Fintype α] [Finite β] (joint : PMF (α × β)) : conditionalEntropy joint = ∑ a : α, ((PMF.map Prod.fst joint) a).toReal * entropy (conditionalSnd joint a)

For any joint law, conditional entropy averages the normalized conditional distributions.

theorem Cslib.Probability.PMF.conditionalEntropy_observe_ge {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Finite β] [Finite γ] (p : PMF α) (kernel : α → PMF β) (observe : α → γ) : ∑ a : α, (p a).toReal * entropy (kernel a) ≤ conditionalEntropy (p.bind fun (a : α) => PMF.map (fun (x : β) => (observe a, x)) (kernel a))

Observing a function of the input leaves at least the average entropy of the output kernel. The observation may merge inputs, including inputs whose conditional laws differ.

theorem Cslib.Probability.PMF.conditionalEntropy_map_fst_ge {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Finite α] [Finite β] [Finite γ] (joint : PMF (α × β)) (observe : α → γ) : conditionalEntropy joint ≤ conditionalEntropy (PMF.map (fun (pair : α × β) => (observe pair.1, pair.2)) joint)

Replacing the observation by a function of it can only increase conditional entropy.

theorem Cslib.Probability.PMF.conditionalEntropy_eq_sum_surprisal {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (joint : PMF (α × β)) : conditionalEntropy joint = ∑ pair : α × β, (joint pair).toReal * surprisal (conditionalSnd joint pair.1) pair.2

Conditional entropy is the expected information content of the hidden value after its observation. Null observations are automatically weighted by zero.

theorem Cslib.Probability.PMF.conditionalEntropy_le_log_card {α : Type u_1} {β : Type u_2} [Finite α] [Fintype β] (joint : PMF (α × β)) : conditionalEntropy joint ≤ Real.logb 2 ↑(Fintype.card β)

Side information leaves at most the logarithm of the unobserved alphabet's size.

theorem Cslib.Probability.PMF.conditionalEntropy_bool_le_one {α : Type u_1} [Finite α] (joint : PMF (α × Bool)) : conditionalEntropy joint ≤ 1

A bit has at most one bit of conditional entropy.

theorem Cslib.Probability.PMF.conditionalEntropy_map_le_of_determined {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Finite β] [Fintype γ] (p : PMF α) (observe : α → β) (value : α → γ) (bad : β → Prop) [DecidablePred bad] (hdetermined : ∀ (x y : α), ¬bad (observe x) → observe x = observe y → value x = value y) : conditionalEntropy (PMF.map (fun (x : α) => (observe x, value x)) p) ≤ ∑ x : α, (p x).toReal * if bad (observe x) then Real.logb 2 ↑(Fintype.card γ) else 0

If an observation determines a value except on bad observations, its remaining entropy is at most the bad probability times the logarithm of the value's alphabet size.

theorem Cslib.Probability.PMF.conditionalEntropy_map_le_collision {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Finite β] [Fintype γ] (p : PMF α) (observe : α → β) (value : α → γ) : conditionalEntropy (PMF.map (fun (x : α) => (observe x, value x)) p) ≤ ∑ x : α, (p x).toReal * if ∃ (y : α), y ≠ x ∧ observe y = observe x then Real.logb 2 ↑(Fintype.card γ) else 0

Entropy can remain only when the observation has more than one possible preimage.

theorem Cslib.Probability.PMF.entropy_chain_rule_deterministic {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Finite α] [Finite β] [Finite γ] (p : PMF α) (f : α → β) (g : α → γ) : entropy (PMF.map f p) + conditionalEntropy (PMF.map (fun (a : α) => (f a, g a)) p) + conditionalEntropy (PMF.map (fun (a : α) => ((f a, g a), a)) p) = entropy p

Exposing a function, then another observation, accounts for all the source entropy.