Relative entropy is a Lyapunov function for a Markov dynamics

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). The general half of the second law at a coarse-graining: what makes a divergence decrease, and what cannot make it decrease.

Mathlib has the three data-processing inequalities for klDiv (klDiv_map_le, klDiv_trim_le, klDiv_comp_right_le). Two consequences that the arrow of time is usually stated as are not there, and this file adds them.

• ★★ klDiv_map_measurableEquiv — a reversible relabelling changes no divergence. The data processing inequality applied in both directions along a measurable equivalence gives equality, so an invertible step produces nothing: whatever a coarse-grained second law produces comes from the coarse-graining or from the kernel, never from a reversible dynamics;
• ★★★ klDiv_comp_le_of_stationary — the H-theorem. If a Markov kernel fixes π, the divergence of any law from π is non-increasing under one step. This is the second law in its modern form: a Lyapunov function, with no symmetry, double stochasticity or detailed balance assumed — only stationarity of the reference;
• Measure.compIterate with ★★ antitone_klDiv_compIterate — and the divergence is monotone along the whole trajectory, which is what makes it an arrow rather than a one-step inequality.

Honest scope

⚠️ No kernel is constructed, and stationarity is a hypothesis. The theorems say what follows from having a Markov kernel with an invariant law; exhibiting one for a given dynamics is the consumer's problem, and the H-theorem is vacuous for a kernel with no invariant measure.

⚠️ Divergence, not Shannon entropy. klDiv q π decreasing is equivalent to Shannon entropy increasing only when π is uniform on a finite space, through klDiv q uniform = log (card) − H q. That identity is not proved here: it needs the Radon–Nikodym derivative of one finite-type measure against another, which is a separate piece of work. Everything below is therefore about divergence from a reference law.

⚠️ klDiv is ∞ off absolute continuity. Both inequalities are then true and empty. The content is for laws absolutely continuous with respect to the reference.

References: T. Cover, J. Thomas, Elements of Information Theory, 2nd ed., Thm 4.4.1 and §11 (relative entropy decreases under a Markov chain with the stationary distribution as reference); Mathlib.InformationTheory.KullbackLeibler.DataProcessing.

The whole trajectory

noncomputable def MeasureTheory.Measure.compIterate {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) (κ : ProbabilityTheory.Kernel α α) : ℕ → Measure α

The law after n steps of a kernel.

Equations

• μ.compIterate κ 0 = μ
• μ.compIterate κ n.succ = (μ.compIterate κ n).bind ⇑κ

@[simp]

theorem MeasureTheory.Measure.compIterate_zero {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) (κ : ProbabilityTheory.Kernel α α) : μ.compIterate κ 0 = μ

@[simp]

theorem MeasureTheory.Measure.compIterate_succ {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) (κ : ProbabilityTheory.Kernel α α) (n : ℕ) : μ.compIterate κ (n + 1) = (μ.compIterate κ n).bind ⇑κ

instance MeasureTheory.Measure.isProbabilityMeasure_compIterate {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [IsProbabilityMeasure μ] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : IsProbabilityMeasure (μ.compIterate κ n)

A reversible step produces nothing

theorem InformationTheory.klDiv_map_measurableEquiv {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (e : α ≃ᵐ β) : klDiv (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑e) ν) = klDiv μ ν

★★ A reversible relabelling changes no divergence. The data processing inequality holds along e and along e.symm, so along a measurable equivalence it is an equality.

This is the half of a coarse-grained second law that is usually left implicit: an invertible step produces no entropy, so whatever a coarse-grained law produces comes from the coarse-graining or from the kernel.

The H-theorem

theorem InformationTheory.klDiv_comp_le_of_stationary {α : Type u_1} {mα : MeasurableSpace α} {μ π : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure π] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (hπ : π.bind ⇑κ = π) : klDiv (μ.bind ⇑κ) π ≤ klDiv μ π

★★★ The H-theorem. If a Markov kernel fixes the reference law π, then the divergence of any law from π is non-increasing under one step of the kernel.

Nothing is assumed beyond stationarity of π: no symmetry, no double stochasticity, no detailed balance. The proof is the data processing inequality with the stationarity rewritten into its right argument.

theorem InformationTheory.antitone_klDiv_compIterate {α : Type u_1} {mα : MeasurableSpace α} {μ π : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsFiniteMeasure π] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (hπ : π.bind ⇑κ = π) : Antitone fun (n : ℕ) => klDiv (μ.compIterate κ n) π

★★ The divergence from a stationary law is monotone along the whole trajectory, which is what makes it an arrow of time rather than a one-step inequality.

theorem InformationTheory.klDiv_compIterate_le {α : Type u_1} {mα : MeasurableSpace α} {μ π : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsFiniteMeasure π] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (hπ : π.bind ⇑κ = π) (n : ℕ) : klDiv (μ.compIterate κ n) π ≤ klDiv μ π

★ And so no step of the trajectory is further from the stationary law than the start.