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 versionsRepository Full 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 101 to 120 of 350 declarations.

lemma

continuous_rdist_restrict_probabilityMeasure

Ruzsa distance depends continuously on the measure.

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

lemma

continuous_rdist_restrict_probabilityMeasure₁

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

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

lemma

tendsto_rdist_probabilityMeasure

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

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

lemma

rdist_le_avg_ent

d[X ; Y] ≤ H[X]/2 + H[Y]/2.

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

lemma

rdist_of_inj

Applying an injective homomorphism does not affect Ruzsa distance.

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

lemma

rdist_zero_eq_half_ent

d[X ; 0] = H[X] / 2.

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

lemma

diff_ent_le_rdist

|H[X] - H[Y]| ≤ 2 d[X ; Y].

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

lemma

If $G$ is an additive group and $X$ is a $G$ -valued random variable and $H\leq G$ is a finite subgroup then, with $\pi:G\to G/H$ the natural homomorphism we have (where $U_H$ is uniform on $H$ ) $\mathbb{H}(\pi(X))\leq 2d[X;U_H].$

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

lemma

rdist_add_const

Adding a constant to a random variable does not change the Rusza distance.

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

lemma

ent_of_diff_le

The improved entropic Ruzsa triangle inequality.

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

lemma

rdist_triangle

The entropic Ruzsa triangle inequality

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

lemma

condRuzsaDist_eq_sum'

Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ in a fintype.

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

lemma

condRuzsaDist_eq_sum

Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ .

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

lemma

condRuzsaDist_nonneg

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

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

lemma

condRuzsaDist'_eq_sum

Explicit formula for conditional Ruzsa distance d[X ; Y | W].

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

lemma

condRuzsaDist'_prod_eq_sum

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

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

lemma

condRuzsaDist'_eq_integral

Explicit formula for conditional Ruzsa distance d[X ; Y | W], in integral form.

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

lemma

condRuzsaDist_of_const

Conditioning by a constant does not affect Ruzsa distance.

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

lemma

condRuzsaDist_of_indep

If $(X,Z)$ and $(Y,W)$ are independent, then d[X | Z ; Y | W] = H[X'- Y' | Z', W'] - H[X'|Z']/2 - H[Y'|W']/2.

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

lemma

condRuzsaDist'_of_indep

Formula for conditional Ruzsa distance for independent sets of variables.

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

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.