Source-linked AI summary
Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory
Fubin Yan, Ruxuan Dong, Ruoxuan Shi, Duolei Wang, Kenneth W. Shum
TL;DR
Rate–distortion theory lacks the formalized infrastructure available for Shannon’s foundational lossless results, despite its role in lossy compression and machine-learning analysis. This paper formalizes core finite-alphabet definitions and the direct and converse theorems in Lean, with reusable components. It also documents that formal verification alone does not ensure alignment between theorem statements and intended mathematics.
Problem
Formalized information-theory libraries remain limited and have focused mainly on Shannon’s lossless results, while reusable Lean infrastructure aligned with standard information-theoretic practice is lacking.
Source: §I · p. 2Method
The paper develops a finite-alphabet Lean library of information measures, supporting results, and coding arguments, then uses it to formalize rate–distortion theorems.
Source: §I · p. 2, D. Verification and reusable components · p. 13Results
The formalization proves the direct result for R > RI(D) and the converse for all distortion thresholds, with achievability also established at R = RI(D) when RI(D) is finite.
Source: §I · p. 2, G. Statements of the direct and… · pp. 7–8Takeaways & Limitations
The work provides reusable definitions and lemmas in Mathlib as a foundation for further formal developments in information theory.
Source: §VII · p. 13, D. Verification and reusable components · p. 13Lean verification alone does not ensure that formal definitions and theorem statements match the intended mathematics, so those statements require careful review.
Source: D. Verification and reusable components · p. 13
Abstract
from arXiv · showhide
Large language models have recently demonstrated an ability to generate substantial mathematical proofs and formalizations, including machine-checked arguments for major open problems and classical theorems. These developments highlight a growing workflow in which AI systems search for proofs while proof assistants certify their correctness. Within information theory, however, formalized libraries remain limited, and existing formalized theorems focus almost exclusively on Shannon's foundational lossless theorems. This paper presents the first Lean formalization of core components of rate-distortion theory, a central framework for lossy compression and modern machine-learning analysis. We identify the alignment challenges that arise when translating information-theoretic definitions, such as distortion measures, typicality and achievability, into a proof-assistant setting, and we develop a reusable library of definitions and lemmas faithful to textbook conventions. Our formalization provides a foundation for future AI-assisted proofs in information theory and enables subsequent mechanized developments to build on a coherent, verified infrastructure rather than generating long proofs from scratch.
I. INTRODUCTION
Rate–distortion theory characterizes the communication rate needed to represent a source under a distortion constraint, but formalized information-theory libraries have focused mainly on Shannon’s lossless results. The paper motivates reusable formalization and lays out the finite-block coding and achievability framework.
I. INTRODUCTION
- Information-theoretic formalization requires definitions and conventions to align with intended mathematics; Lean verifies proofs against formal statements, not that correspondence itself.The paper also identifies limited reuse of long AI-generated proofs as motivation for a library aligned with standard practice.Source: §I · pp. 1–2
- Formalized information-theory results have focused primarily on Shannon’s foundational lossless theorems, leaving rate–distortion theory without mainstream proof-assistant formalization.Rate–distortion theory concerns the minimum communication rate for representing a source subject to a prescribed distortion constraint.Source: §I · p. 2
- The paper initiates a Lean formalization of finite-alphabet rate–distortion theory, proving direct and converse results and developing reusable definitions and lemmas.It also establishes optimal test-channel existence and right continuity of the information rate–distortion function.Source: §I · p. 2
II. PROBLEM FORMULATION
- An (n, M) code encodes a length-n source sequence into one of M indices, which the decoder maps to a reproduction sequence; its rate is log2 M/n.The rate–distortion formulation evaluates such codes under a distortion constraint.Source: §II · p. 2
- The formulation allows a general joint distribution on source blocks and defines achievability through a sequence of increasingly long codes with rates bounded by R.The paper notes that its limsup-based criterion is more flexible than a limit-based definition.Source: §II · p. 3
- An alternate fidelity criterion requires distortion below D + ϵ with probability at least 1 − δ for positive ϵ and δ.The cited discussion calls this source coding with a fidelity criterion.Source: §II · p. 3
A. Information rate-distortion function
The information rate–distortion function minimizes mutual information over conditional distributions that meet an expected-distortion constraint. The section describes its boundary behavior and standard properties for finite alphabets.
A. Information rate-distortion function
- The information rate–distortion function is the minimum mutual information over conditional distributions whose expected distortion is at most D.With finite alphabets, the feasible optimization is attained by at least one conditional distribution.Source: A. Information rate-distortion function · p. 3
- For D ≥ Dmax, a constant reproduction symbol achieves the distortion with zero rate; for D < Dmin, the function is infinite.Dmax is the smallest attainable average distortion using a constant decoder output, while Dmin is the smallest possible distortion.Source: A. Information rate-distortion function · p. 4
- For a finite source alphabet, the information rate–distortion function is strictly decreasing between Dmin and Dmax and convex for D ≥ Dmin.The section also states that the achievable rate–distortion region lies above the curve R = RI(D).Source: A. Information rate-distortion function · p. 4
- For finite alphabets and bounded distortion, rates above RI(D) are achievable, whereas rates below RI(D) are not.The source symbols are modeled as independent draws from a known distribution in the section’s simplest probability model.Source: A. Information rate-distortion function · pp. 3–4
III. LEAN FORMALIZATION OF INFORMATION MEASURES
The formalization represents finite-alphabet distributions with Mathlib’s PMF type and defines standard information measures using finite sums and Mathlib’s measure-theoretic infrastructure. It handles zero-probability and support cases explicitly.
III. LEAN FORMALIZATION OF INFORMATION MEASURES
- The development assumes finite source and reproduction alphabets, represented by finite types with decidable equality; a PMF assigns nonnegative weights summing to one.Mathlib stores probabilities as extended nonnegative reals, which are converted to reals when entropy calculations require logarithms.Source: §III · p. 4
A. Entropy
- Shannon entropy is encoded as the standard finite-alphabet sum, using the natural logarithm and Mathlib’s negated p log p operation.At probability zero, Mathlib’s log convention makes the entropy summand zero, matching the standard convention.Source: A. Entropy · p. 4
B. Joint entropy
- Joint entropy is represented as entropy applied to a distribution on the product alphabet.The formalization uses a wrapper around the entropy definition for the joint distribution.Source: B. Joint entropy · p. 5
C. KL divergence and mutual information
- KL divergence uses Mathlib’s measure-theoretic definition and takes the value +∞ when positive mass under P lies outside the support of Q.The definition handles zero P-mass terms as zero and positive P-mass paired with zero Q-mass as infinite.Source: C. KL divergence and mutual information · p. 5
- Mutual information is defined as the KL divergence between the joint distribution and the product of its marginals.The marginals come from mapping the joint PMF to each coordinate, and the independent product PMF is built with bind and map.Source: C. KL divergence and mutual information · p. 5
- The formalization’s definitions closely follow textbook conventions while using Mathlib’s infrastructure for entropy, KL divergence, and mutual information.This summarizes the stated encoding of the measures rather than adding a separate theorem claim.Source: C. KL divergence and mutual information · p. 5
IV. DEFINING THE RATE–DISTORTION FUNCTION
The rate–distortion function is formalized through conditional distributions, expected distortion, and an infimum over feasible channels. The Lean development also encodes block codes and finite-alphabet distortion conventions.
IV. DEFINING THE RATE–DISTORTION FUNCTION
- A test channel assigns a conditional distribution on Y to each source symbol x, represented in Lean as a function X → PMF Y.The function is defined for a fixed source distribution and distortion function.Source: §IV · p. 5
A. Distortion function and single-letter expected distortion
- The single-letter expected distortion averages d(x, y) over the source PMF and the test-channel output distribution.Distortion values are modeled as nonnegative finite reals and embedded in ENNReal for the expectation.Source: A. Distortion function and… · p. 5
B. Induced joint distribution
- The induced joint distribution samples x from P and then y from W(· | x), producing the pair (x, y).The Lean implementation builds this distribution with bind and map.Source: B. Induced joint distribution · p. 5
C. Information rate–distortion function
- The rate–distortion function is the infimum of mutual-information values for test channels satisfying the expected-distortion bound.If no channel meets the constraint, the infimum is +∞ in ENNReal.Source: C. Information rate–distortion function · p. 6
V. FORMALIZATION OF THE RATE DISTORTION PROBLEM
- The formalization aims to mirror textbook definitions for finite alphabets, block codes, average distortion, i.i.d. sources, and asymptotic achievability.These are the stated components of the rate–distortion problem encoded in Lean.Source: §V · p. 6
A. Distortion measures
- Block length n and codebook size M are positive parameters; length-n blocks are functions on Fin n and codeword indices belong to Fin M.The positivity assumptions support later arguments involving divisions and nonempty codebooks.Source: A. Distortion measures · p. 6
B. Rate–distortion codes
The section formalizes finite-alphabet rate–distortion codes and the quantities used to evaluate them. It defines average block distortion and code rate, then models i.i.d. source blocks and the code’s expected distortion.
B. Rate–distortion codes
- A rate–distortion code pairs an encoder from source blocks to a finite index set with a decoder from that set to reproduction blocks.Lean packages the encoder and decoder together in a structure.Source: B. Rate–distortion codes · p. 6
C. Block distortion and code rate
- Block distortion is the sum of coordinate-wise distortions divided by the positive blocklength, while code rate is log M divided by blocklength.The coordinate sum ranges over Fin n.Source: C. Block distortion and code rate · p. 6
D. Discrete memoryless source model and expected distortion
- The source model assigns each block the product of its single-letter probabilities and packages these probabilities as an i.i.d. block PMF.Expected distortion averages the distortion after encoding and decoding against that block distribution.Source: D. Discrete memoryless source model… · pp. 6–7
E. Sequences of codes and asymptotic distortion
The section defines sequences of positive-length codes, their asymptotic expected distortion, and rate–distortion achievability under a rate cap on every code. It states the direct and converse theorem for finite alphabets and finite-valued nonnegative distortion.
E. Sequences of codes and asymptotic distortion
- A code sequence uses an (n + 1, M_n) code at each index, ensuring positive blocklength, and its asymptotic expected distortion is the limit superior of expected distortions.The limit superior is expressed with Mathlib filters along atTop.Source: E. Sequences of codes and asymptotic… · p. 7, -- A sequence of codes with positive · p. 7
F. Achievability of rate–distortion pairs
- Achievability requires a code sequence whose asymptotic expected distortion is at most D and whose rate for every code is at most R.The definition combines separate distortion and pointwise-rate constraints.Source: F. Achievability of rate–distortion… · p. 7, -- Every code satisfies the prescribed… · p. 7, -- Achievability with a pointwise rate · p. 7
G. Statements of the direct and converse theorems
- For finite alphabets and finite-valued nonnegative distortion, R > RI(D) makes (R, D) achievable, while achievability requires R ≥ RI(D), so R < RI(D) is impossible.The distortion is bounded under these assumptions, so no separate boundedness hypothesis is needed.Source: G. Statements of the direct and… · pp. 7–8
VI. PROOF OF THE RATE–DISTORTION THEOREM
The proof roadmap begins with the shorter converse, then establishes achievability above the rate–distortion function under a pointwise rate bound. It also proves an equality-threshold result under a weaker asymptotic rate constraint and identifies reusable verified components.
VI. PROOF OF THE RATE–DISTORTION THEOREM
- The converse is presented first because its proof involves fewer steps.Source: §VI · p. 8
- The proof establishes achievability for R > RI(D) while requiring every code to satisfy the prescribed rate bound.Source: §VI · p. 8
- At R = RI(D), achievability is additionally proved when the rate bound is required only in the limit superior.The section also discusses verification and reusable components.Source: §VI · p. 8
A. Converse
The converse derives a rate lower bound from the distortion constraint, first at finite blocklength and then asymptotically. Right continuity of the rate–distortion function removes the positive distortion slack and yields the pointwise converse.
A. Converse
- For a length-n code, the finite-block inequality is RI(Dn) ≤ log M/n, where Dn is expected distortion and log M/n is code rate.The bound uses feasibility of the average joint distribution and a mutual-information bound.Source: A. Converse · p. 8
- For any positive distortion slack ε, the sequence converse bounds RI(D + ε) by the limit-superior code rate when asymptotic distortion is at most D.The proof uses the finite-block inequality and the distortion limit-superior bound.Source: A. Converse · p. 9
- A pointwise rate bound implies the corresponding limit-superior rate bound, so pointwise achievability implies asymptotic-rate achievability.The pointwise converse converts this implication and uses the proved right continuity, requiring no separate continuity hypothesis.Source: A. Converse · p. 9
- Finite alphabets make the test-channel space compact, and continuity of expected distortion and mutual information yields lower semicontinuity and right continuity of RI.Source: A. Converse · p. 9
- Right continuity removes the positive slack, giving RI(D) ≤ R for asymptotically achievable pairs.The proof first derives the bound at D + ε.Source: A. Converse · p. 9
B. Random-coding achievability
The section proves strict-rate achievability by random coding: it bounds the probability that a random codebook has no suitable codeword, selects deterministic codes, and removes distortion slack to obtain an asymptotic code sequence.
B. Random-coding achievability
- The codebook independently samples M codewords from the test channel’s output-marginal distribution, and the encoder selects a codeword meeting distortion and information-density thresholds.If no codeword meets the general good-pair predicate, the encoder returns index 0.Source: B. Random-coding achievability · p. 10
- Chebyshev estimates make the joint good-pair probability high for thresholds D + η and na, where η > 0 and I(P, W) < a < R.A change-of-measure bound and codeword independence then control the chance that all codewords fail.Source: B. Random-coding achievability · pp. 10–11
- Averaging over codebooks yields a deterministic code with bounded expected distortion, since a good codeword incurs at most D + η and a miss incurs at most dmax.For fixed η and δ, the finite-block conclusion holds at every sufficiently large blocklength.Source: B. Random-coding achievability · p. 11
- For a feasible test channel with mutual information below R, the construction yields a code sequence with pointwise rate at most R and asymptotic distortion at most D.The finite-block estimates are combined by diagonal selection to remove distortion slack.Source: B. Random-coding achievability · p. 12
- When D = +∞, a constant-reconstruction code with one codeword satisfies the rate bound at every blocklength.In this case there is no distortion restriction.Source: B. Random-coding achievability · p. 12
C. Achievability at the equality rate
At the equality rate, the proof handles positive and zero rates separately. For positive rates it introduces a small distortion slack to create a test channel with mutual information strictly below the fixed rate, then removes the slack; the zero-rate case uses constant reconstruction.
C. Achievability at the equality rate
- For R > 0, mixing an optimal test channel with an independent reproduction channel gives mutual information strictly below R while increasing distortion by an arbitrarily small amount.The mixing parameter controls the added distortion.Source: C. Achievability at the equality rate · p. 12
- Applying random-coding estimates at the fixed rate R and then using diagonal selection removes the distortion errors and yields an asymptotic code sequence.The channel mixture contributes additional distortion that also tends to zero.Source: C. Achievability at the equality rate · p. 12
- When R = 0, a symbol selected from an optimal zero-mutual-information test channel gives codes with one codeword and expected average distortion at most D.The induced joint distribution is the product of its marginals.Source: C. Achievability at the equality rate · p. 12
- For positive R with finite D and finite rate-distortion value, the theorem establishes pointwise achievability at R = RI(D).The proof also handles D = +∞ with constant-reconstruction codes.Source: C. Achievability at the equality rate · pp. 12–13
D. Verification and reusable components
The paper checks theorem statements against their intended mathematics before using AI assistance to complete proofs, then verifies the Lean development. It also supplies reusable information-theoretic and coding components built on Mathlib.
D. Verification and reusable components
- Definitions, hypotheses, quantifiers, and conclusions were checked against their mathematical counterparts before AI assistance completed the proofs.Lean then checked the resulting proof.Source: D. Verification and reusable components · p. 13
- The Lean module compiles without sorry placeholders, and the audited main results use only propext, Classical.choice, and Quot.sound, with no dependency on sorryAx.The authors inspect these dependencies with #print axioms.Source: D. Verification and reusable components · p. 13
- The reusable library covers finite-alphabet information measures, optimization over test channels, coding arguments, and results including continuity and optimal-channel existence.The development reuses Mathlib definitions and results wherever possible.Source: D. Verification and reusable components · p. 13
- Random-codebook sampling, a general-predicate encoder, and diagonal construction package probability and limit arguments for later developments.The stated aim is to support formalization of further results.Source: D. Verification and reusable components · p. 13
VII. CONCLUDING REMARKS
The paper formalizes the finite-alphabet rate-distortion theorem in Lean, making its objects, assumptions, and conventions explicit. It presents this infrastructure as a basis for further formal developments in information theory.
VII. CONCLUDING REMARKS
- The described prospective workflow has researchers specify problems formally, AI systems produce machine-certified proofs, and mathematicians interpret those proofs.The paper argues that basic information-theoretic results must first be formalized for this approach to be applied in the field.Source: §VII · p. 13
- The development proves the direct and converse parts of the finite-alphabet rate-distortion theorem in Lean and provides reusable definitions and lemmas built on Mathlib.It makes explicit conventions for zero-probability events, extended nonnegative real values, and feasibility constraints.Source: §VII · p. 13
- Future work may extend the foundations to rate-distortion–perception tradeoffs and their applications in machine learning and communication.The paper frames the infrastructure as supporting machine-checkable proofs while preserving conceptual clarity.Source: §VII · p. 13