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 281 to 300 of 350 declarations.

lemma

rho_of_subgroup

If HH is a finite subgroup of GG, and ρ(UH)≤r\rho(U_H) \leq r, then there exists tt such that ∣A∩(H+t)∣≥e−r∣A∣∣H∣|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}, and ∣H∣/∣A∣∈[e−2r,e2r]|H|/|A| \in [e^{-2r}, e^{2r}].

PFR.RhoFunctional · PFR/RhoFunctional.lean:679

lemma

rhoMinus_of_sum

If X,YX,Y are independent, one has ρ−(X+Y)≤ρ−(X) \rho^-(X+Y) \leq \rho^-(X)

PFR.RhoFunctional · PFR/RhoFunctional.lean:763

lemma

condRho_of_injective

If ff is injective, then ρ(X∣f(Y))=ρ(X∣Y)\rho(X|f(Y))=\rho(X|Y).

PFR.RhoFunctional · PFR/RhoFunctional.lean:889

lemma

condRho_eq_of_identDistrib

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

PFR.RhoFunctional · PFR/RhoFunctional.lean:906

lemma

condRhoMinus_le

ρ−(X∣Z)≤ρ−(X)+\bbH[X]−\bbH[X∣Z] \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]

PFR.RhoFunctional · PFR/RhoFunctional.lean:932

lemma

condRhoPlus_le

ρ+(X∣Z)≤ρ+(X) \rho^+(X|Z) \leq \rho^+(X)

PFR.RhoFunctional · PFR/RhoFunctional.lean:960

lemma

condRho_prod_eq_sum

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

PFR.RhoFunctional · PFR/RhoFunctional.lean:994

lemma

condRho_prod_le

ρ(X∣Z)≤ρ(X)+12(\bbH[X]−\bbH[X∣Z]) \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z]), conditional version

PFR.RhoFunctional · PFR/RhoFunctional.lean:1020

lemma

condRho_prod_eq_of_indepFun

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

PFR.RhoFunctional · PFR/RhoFunctional.lean:1040

lemma

rho_of_sum_le

If X,YX,Y are independent, then ρ(X+Y)≤12(ρ(X)+ρ(Y)+d[X;Y]). \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).

PFR.RhoFunctional · PFR/RhoFunctional.lean:1064

lemma

condRho_of_sum_le

If X,YX,Y are independent, then ρ(X∣X+Y)≤12(ρ(X)+ρ(Y)+d[X;Y]). \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).

PFR.RhoFunctional · PFR/RhoFunctional.lean:1079

lemma

phi_min_exists

There exists a ϕ\phi-minimizer.

PFR.RhoFunctional · PFR/RhoFunctional.lean:1160

lemma

le_rdist_of_phiMinimizes

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

PFR.RhoFunctional · PFR/RhoFunctional.lean:1207

lemma

I_one_le

I1≤2ηd[X1;X2]I_1\le 2\eta d[X_1;X_2]

PFR.RhoFunctional · PFR/RhoFunctional.lean:1301

lemma

rdist_add_rdist_eq

d[X1;X1]+d[X2;X2]=2d[X1;X2]+(I2−I1)d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1).

PFR.RhoFunctional · PFR/RhoFunctional.lean:1388

lemma

I_two_le

I2≤2ηd[X1;X2]+η1−η(2ηd[X1;X2]−I1)I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1).

PFR.RhoFunctional · PFR/RhoFunctional.lean:1415

lemma

dist_le_of_sum_zero

If GG-valued random variables T1,T2,T3T_1,T_2,T_3 satisfy T1+T2+T3=0T_1+T_2+T_3=0, then

+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$

PFR.RhoFunctional · PFR/RhoFunctional.lean:1459

lemma

dist_le_of_sum_zero_cond

If GG-valued random variables T1,T2,T3T_1,T_2,T_3 satisfy T1+T2+T3=0T_1+T_2+T_3=0, then

+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$

PFR.RhoFunctional · PFR/RhoFunctional.lean:1501

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.