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 221 to 240 of 350 declarations.

lemma

ProbabilityTheory.swap_condDistrib_ae_eq

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

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:339

lemma

ProbabilityTheory.condDistrib_const_unit

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

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:357

lemma

ProbabilityTheory.map_compProd_condDistrib

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

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:391

lemma

kvm_ineq_I

If n ≥ 0 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then H[Y i₀ + ∑ i ∈ s, Y i; μ] - H[Y i₀; μ] ≤ ∑ i ∈ s, (H[Y i₀ + Y i; μ] - H[Y i₀; μ]).

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:301

lemma

kvm_ineq_II

If n ≥ 1 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ].

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:342

lemma

kvm_ineq_III

If n ≥ 1 and X, Y₁, ..., Yₙ$ are jointly independent G-valued random variables, then d[Y i₀, ∑ i, Y i] ≤ d[Y i₀, Y i₁] + 2⁻¹ * (H[∑ i, Y i] - H[Y i₁]).

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:464

lemma

ent_of_sum_le_ent_of_sum

Let X₁, ..., Xₘ and Y₁, ..., Yₗ be tuples of jointly independent random variables (so the X's and Y's are also independent of each other), and let f : {1,..., l} → {1,... ,m} be a function, then H[∑ j, Y j] ≤ H[∑ i, X i] + ∑ j, H[Y j - X f(j)] - H[X_{f(j)}].

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:633

lemma

ent_sub_zsmul_le

Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer. Then H[X - (a+1)Y] ≤ H[X - aY] + H[X - Y - X'] - H[X]

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:686

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.