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 121 to 140 of 350 declarations.

lemma

condRuzsaDist_of_copy

The conditional Ruzsa distance is unchanged if the sets of random variables are replaced with copies.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:830

lemma

condRuzsaDist'_of_copy

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:905

lemma

condRuszaDist_prod_eq_of_indepFun

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:956

lemma

condRuzsaDist_comp_right

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:977

lemma

condRuzsaDist_of_inj_map

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:992

lemma

condRuzsaDist'_of_inj_map

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1015

lemma

condRuzsaDist'_of_inj_map'

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1053

lemma

kaimanovich_vershik

The Kaimanovich-Vershik inequality. H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y].

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1114

lemma

kaimanovich_vershik'

A version of the Kaimanovich-Vershik inequality with some variables negated.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1146

lemma

ent_bsg

The entropic Balog-Szemerédi-Gowers inequality. Let A, B be G-valued random variables on Ω, and set Z := A+B. Then ∑ z, P[Z=z] d[(A | Z = z) ; (B | Z = z)] ≤ 3 I[A :B] + 2 H[Z] - H[A] - H[B]. TODO: remove the hypothesis of Fintype G from here and from condIndep_copies'

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1166

lemma

condRuzsaDist_le

Suppose that (X,Z)(X, Z) and (Y,W)(Y, W) are random variables, where X,YX, Y take values in an abelian group. Then d[X∣Z;Y∣W]≤d[X;Y]+12I[X:Z]+12I[Y:W]d[X | Z ; Y | W] \leq d[X ; Y] + \tfrac{1}{2} I[X : Z] + \tfrac{1}{2} I[Y : W]

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1291

lemma

condRuzsaDist_le'_prod

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1336

lemma

comparison_of_ruzsa_distances

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1352

lemma

condRuzsaDist_diff_ofsum_le

Open the record for the exact Lean statement and complete source.

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1433

lemma

ProbabilityTheory.setRuzsaDist_of_inj

Ruzsa distance between sets is preserved by injective homomorphisms.

PFR.ForMathlib.Entropy.RuzsaSetDist · PFR/ForMathlib/Entropy/RuzsaSetDist.lean:90

lemma

ProbabilityTheory.setRuzsaDist_le

Ruzsa distance between sets is controlled by the doubling constant.

PFR.ForMathlib.Entropy.RuzsaSetDist · PFR/ForMathlib/Entropy/RuzsaSetDist.lean:110

lemma

ProbabilityTheory.sum_meas_smul_cond_fiber'

The law of total probability for a random variable taking finitely many values: a measure μ can be expressed as a linear combination of its conditional measures μ[|X ← x] on fibers of a random variable X valued in a fintype.

PFR.ForMathlib.FiniteRange.ConditionalProbability · PFR/ForMathlib/FiniteRange/ConditionalProbability.lean:18

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.