InformationTheory.Fano.Entropy

Imports 5

Single-variable Shannon entropy #

Non-negativity on [0, 1] masses, the support-restricted maximum-entropy bound (Jensen on Real.negMulLog), the universe-wide specialization, and the Dirac-collapse identity.

Implementation notes #

entropyOfFn is the mass-function form (a sum over α → ℝ) used by the Fano.Core development. The measure-theoretic developments (Shannon.Bridge.entropy, InformationTheory.MeasureFano.condEntropy) use a parallel formalism; the two do not depend on each other.

noncomputable def

InformationTheory.entropyOfFn

source

{α : Type u_1} [Fintype α] (μ : α → ℝ) :

ℝ

Shannon entropy (in nats) of a real-valued mass function on a finite type.

Equations

InformationTheory.entropyOfFn μ = ∑ a : α, (μ a).negMulLog

Instances For

Used by

theorem

InformationTheory.entropyOfFn_nonneg

source

{α : Type u_1} [Fintype α] (μ : α → ℝ) (h0 : ∀ (a : α), 0 ≤ μ a) (h1 : ∀ (a : α), μ a ≤ 1) :

0 ≤ entropyOfFn μ

Shannon entropy is non-negative whenever each mass lies in [0, 1].

Used by

theorem

InformationTheory.entropyOfFn_le_log_supportCard

source

{α : Type u_1} [Fintype α] (μ : α → ℝ) (hμ : ∀ (a : α), 0 ≤ μ a) (hsum : ∑ a : α, μ a = 1) {S : Finset α} (hsupp : ∀ a ∉ S, μ a = 0) :

entropyOfFn μ ≤ Real.log ↑S.card

Maximum-entropy bound, restricted to a Finset containing the support: a probability mass function whose support is contained in S has Shannon entropy at most log S.card.

Used by

theorem

InformationTheory.entropyOfFn_le_log_card

source

{α : Type u_1} [Fintype α] (μ : α → ℝ) (hμ : ∀ (a : α), 0 ≤ μ a) (hsum : ∑ a : α, μ a = 1) :

entropyOfFn μ ≤ Real.log ↑(Fintype.card α)

The maximum-entropy bound: a probability mass function on a finite type of cardinality n has Shannon entropy at most log n.

Used by

theorem

InformationTheory.entropyOfFn_eq_zero_of_isDirac

source

{α : Type u_1} [Fintype α] [DecidableEq α] (μ : α → ℝ) (a₀ : α) (h : ∀ (a : α), μ a = if a = a₀ then 1 else 0) :

entropyOfFn μ = 0

A Dirac mass at a₀ has zero Shannon entropy.

Used by