Skip to main content
therefore
Sign inSign up
Open navigation
All packages

teorth/PFR

PFR

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

Therefore indexed 350 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.

Research project222 GitHub starsApache-2.023 indexed versionsRepositoryFull history on Reservoir
mathadditive-combinatoricsinformation-theory

Head version

v4.33.0-rc1

a177b2e4abe4b31c8024b9afebe646bf6bb8f91b

Toolchain
leanprover/lean4:v4.33.0-rc1
Revision date
16 Jul 2026
Dependencies
11
Versions
23

External build observation

Exact head commit and toolchain

Reservoir recorded build status passed and test status not observed for commit a177b2e4abe4 with leanprover/lean4:v4.33.0-rc1 on 20 Jul 2026. Therefore did not run this build.

Pin this source in lakefile.lean

require PFR from git "https://github.com/teorth/pfr.git" @ "a177b2e4abe4b31c8024b9afebe646bf6bb8f91b"

Source declarations

350 indexed proofs

Package history

Showing 41 to 60 of 350 declarations.

lemma

ProbabilityTheory.condEntropy_of_injective

If X : Ω → S, Y : Ω → T are random variables, and f : T × S → U is injective for each fixed t ∈ T, then H[f(Y, X) | Y] = H[X | Y]. Thus for instance H[X-Y|Y] = H[X|Y].

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:506

lemma

ProbabilityTheory.chain_rule'

One form of the chain rule : H[X, Y] = H[X] + H[Y | X].

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:547

lemma

ProbabilityTheory.cond_chain_rule'

If X : Ω → S, Y : Ω → T, Z : Ω → U are random variables, then H[X, Y | Z] = H[X | Z] + H[Y|X, Z].

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:618

lemma

ProbabilityTheory.entropy_comp_le

Data-processing inequality for the entropy: H[f(X)] ≤ H[X]. To upgrade this to equality, see entropy_of_comp_eq_of_comp or entropy_comp_of_injective.

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:643

lemma

ProbabilityTheory.condEntropy_comp_ge

Data-processing inequality for the conditional entropy: H[Y|f(X)] ≥ H[Y|X] To upgrade this to equality, see condEntropy_of_injective'

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:1095

lemma

ProbabilityTheory.condMutual_comp_comp_le

Let X, Y, Z. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ].

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:1167

lemma

ProbabilityTheory.max_entropy_le_entropy_prod

If X₁, ..., Xₙ are independent and s ⊆ {1, ..., n}, then for all i ∈ s, H[Xᵢ] ≤ H[∏ j ∈ s, Xⱼ].

PFR.ForMathlib.Entropy.Group · PFR/ForMathlib/Entropy/Group.lean:248

Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.