Polynomial Freiman-Ruzsa

The blueprint of Polynomial Freiman-Ruzsa, read at commit 1ef23c3c (2026-11-05): one article for each of its 213 nodes whose Lean declarations it names and marks formalized, or in Mathlib. Its other 6 nodes have no article, and a section of only those is left out: the map records what the project contains, not what it plans. A statement for which the blueprint marks no proof \leanok says so. Dependencies are the blueprint's \uses: a statement's under Depends on, a proof's under Proof depends on.

The text is the blueprint's, under its Apache-2.0 license: each page has a section's prose, remarks and examples in the blueprint's order, with each node's statement and proof where the node stands.

• Applications of Jensen's inequality
• Shannon entropy inequalities
• Entropic Ruzsa calculus
• The 100% version of PFR
• The Fibring lemma
• Entropy version of PFR
• Proof of PFR
• Improving the exponents
• Homomorphism version of PFR
• Approximate homomorphism version of PFR
• Weak PFR over the integers
• The \(m\)-torsion case
• Further improvement to exponent

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.