Shannon entropy on a finite type, and the H-theorem in entropy form

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #110, the residue #109 named.

Mathlib has the Kullback–Leibler divergence but no Shannon entropy of a measure — not for a finite type, not anywhere. #109 proved the arrow of time in its divergence form, which is the general one; this file supplies the identity that turns it into the textbook statement, and the two classical consequences.

What is proved

• measureEntropy μ = ∑ x, negMulLog (μ.real {x}) — Shannon entropy of a measure on a finite type;
• ★★ withDensity_uniformOn_univ — the density of a measure against the uniform law is card · μ{x}, which is the Radon–Nikodym computation the identity needs and the only real work here. It holds for any measure on a finite type, not only a probability measure, and so do absolutelyContinuous_uniformOn_univ and ★★ llr_uniformOn_univ_ae — hence the log-likelihood ratio against the uniform law is log (card · μ{x}) almost everywhere;
• ★★★ integral_llr_uniformOn_univ and ★★★ klDiv_uniformOn_univ — the identity: klDiv μ uniform = ENNReal.ofReal (log card − measureEntropy μ). The vanishing of the two correction terms is what makes it clean: both measures are probability measures;
• ★★ measureEntropy_le_log_card — the maximum-entropy theorem, from Gibbs' inequality, and ★ measureEntropy_uniformOn_univ — the uniform law attains it, so the bound is tight;
• ★★★ monotone_measureEntropy_compIterate — the H-theorem in entropy form: under a Markov kernel that fixes the uniform law, Shannon entropy is non-decreasing, monotonically along the whole trajectory. This is the classical statement, and it is #109's divergence form composed with the identity above.

Honest scope

⚠️ The uniform reference is not optional. Entropy increases along a kernel that fixes the uniform law; a kernel with some other stationary law moves entropy either way, and what is monotone then is the divergence from that law (#109), not the entropy. The two statements coincide only here.

⚠️ Finite type only. measureEntropy sums over Fintype.card α point masses. Differential entropy, countable types with infinite entropy, and the conditional and joint entropies are all untouched.

⚠️ No convergence, and no rate. Monotone is not strictly increasing, and nothing says the entropy reaches log card: a kernel can be the identity.

References: T. Cover, J. Thomas, Elements of Information Theory, 2nd ed., Thm 2.6.4 (maximum entropy) and §4.4 (the H-theorem for a doubly stochastic chain); Mathlib.InformationTheory.KullbackLeibler.Basic (klDiv, llr, integral_llr_add_sub_measure_univ_nonneg = Gibbs), Mathlib.Probability.UniformOn; KlDivArrow.lean (#109's Cat-1 half).

theorem InformationTheory.card_ne_zero_ennreal (α : Type u_1) [Fintype α] [Nonempty α] : ↑(Fintype.card α) ≠ 0

theorem InformationTheory.card_ne_zero_real (α : Type u_1) [Fintype α] [Nonempty α] : ↑(Fintype.card α) ≠ 0

noncomputable def InformationTheory.measureEntropy {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ : MeasureTheory.Measure α) : ℝ

Shannon entropy of a measure on a finite type: −∑ p log p over the point masses.

Equations

• InformationTheory.measureEntropy μ = ∑ x : α, (μ.real {x}).negMulLog

instance InformationTheory.isProbabilityMeasure_uniformOn_univ {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn Set.univ)

theorem InformationTheory.uniformOn_univ_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] (x : α) : (ProbabilityTheory.uniformOn Set.univ) {x} = (↑(Fintype.card α))⁻¹

theorem InformationTheory.measureReal_uniformOn_univ_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] (x : α) : (ProbabilityTheory.uniformOn Set.univ).real {x} = (↑(Fintype.card α))⁻¹

theorem InformationTheory.measure_eq_sum_restrict_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] (μ : MeasureTheory.Measure α) (s : Set α) : μ s = ∑ x : α, (μ.restrict s) {x}

Every measure on a finite type is the sum of its point masses, restricted.

theorem InformationTheory.sum_measureReal_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : ∑ x : α, μ.real {x} = 1

The density against the uniform law

theorem InformationTheory.withDensity_uniformOn_univ {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) : ((ProbabilityTheory.uniformOn Set.univ).withDensity fun (x : α) => ↑(Fintype.card α) * μ {x}) = μ

★★ The density of a law against the uniform law is card · μ{x}. This is the Radon–Nikodym computation the entropy identity runs on, and the only real work in this file.

theorem InformationTheory.absolutelyContinuous_uniformOn_univ {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) : μ.AbsolutelyContinuous (ProbabilityTheory.uniformOn Set.univ)

theorem InformationTheory.llr_uniformOn_univ_ae {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) : MeasureTheory.llr μ (ProbabilityTheory.uniformOn Set.univ) =ᵐ[μ] fun (x : α) => Real.log (↑(Fintype.card α) * μ.real {x})

★★ So the log-likelihood ratio against the uniform law is log (card · μ{x}), almost everywhere.

The identity, and the two classical consequences

theorem InformationTheory.integral_llr_uniformOn_univ {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : ∫ (x : α), MeasureTheory.llr μ (ProbabilityTheory.uniformOn Set.univ) x ∂μ = Real.log ↑(Fintype.card α) - measureEntropy μ

★★★ The entropy identity, in integral form.

theorem InformationTheory.klDiv_uniformOn_univ {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : klDiv μ (ProbabilityTheory.uniformOn Set.univ) = ENNReal.ofReal (Real.log ↑(Fintype.card α) - measureEntropy μ)

★★★ The identity: the divergence from the uniform law is log card − entropy. The two correction terms in klDiv's definition vanish because both measures are probability measures.

theorem InformationTheory.measureEntropy_le_log_card {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : measureEntropy μ ≤ Real.log ↑(Fintype.card α)

★★ The maximum-entropy theorem: no law on a finite type has entropy above log card. This is Gibbs' inequality read through the identity.

theorem InformationTheory.measureEntropy_uniformOn_univ {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] : measureEntropy (ProbabilityTheory.uniformOn Set.univ) = Real.log ↑(Fintype.card α)

★ And the uniform law attains it, so the bound is tight.

The H-theorem in entropy form

theorem InformationTheory.monotone_measureEntropy_compIterate {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α] [Nonempty α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (hκ : (ProbabilityTheory.uniformOn Set.univ).bind ⇑κ = ProbabilityTheory.uniformOn Set.univ) : Monotone fun (n : ℕ) => measureEntropy (μ.compIterate κ n)

★★★ The H-theorem in entropy form. Under a Markov kernel that fixes the uniform law, Shannon entropy is non-decreasing, monotonically along the whole trajectory.

This is the classical statement, and it is #109's divergence form (antitone_klDiv_compIterate) composed with the identity: klDiv · uniform and measureEntropy move in opposite directions, and the maximum-entropy bound is what licenses stripping ENNReal.ofReal.