Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 45 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

45 results

Clear filters
Project-declaredLean 4.33.0-rc1

PFR conjecture

PFR_conjecture

Plain-language statement

The polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most K, then A can be covered by at most 2 * K ^ 12 cosets of a subgroup of cardinality at most |A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture improv

PFR_conjecture_improv

Project documentation

Improved polynomial Freiman-Ruzsa theorem. Let AA be a nonempty subset of a finite elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a subspace HH and a set of representatives cc such that Ac+HA\subseteq c+H, c<2K11|c|<2K^{11}, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture improv

PFR_conjecture_improv'

Project documentation

Improved polynomial Freiman-Ruzsa theorem without a finite ambient-group assumption. Let AA be a nonempty finite subset of an elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a finite subspace HH and a finite set cc such that Ac+HA\subseteq c+H, c<2K11|c|<2K^{11}, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

PFR conjecture

PFR_conjecture'

Project documentation

Polynomial Freiman-Ruzsa theorem without a finite ambient-group assumption. Let AA be a nonempty finite subset of an elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a finite subspace HH and a finite set cc such that Ac+HA\subseteq c+H, c<2K12|c|<2K^{12}, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Probability Theory i Indep Fun sum elim

ProbabilityTheory.iIndepFun.sum_elim

Plain-language statement

Two internally independent families remain jointly independent after they are combined over a disjoint union, provided the two family-valued random variables are independent of one another.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Rdist add rdist add cond Mutual eq

rdist_add_rdist_add_condMutual_eq

Plain-language statement

A fibring identity in the τ\tau-minimizer setup. Let X1,X2X_1',X_2' be independent copies of X1,X2X_1,X_2 and put k=d[X1;X2]k=d[X_1;X_2]. Then d[X1+X2;X2+X1]+d[X1X1+X2;X2X2+X1]+I[X1+X2:X1+X2X1+X2+X1+X2]=2kd[X_1+X_2';X_2+X_1']+d[X_1\mid X_1+X_2';X_2\mid X_2+X_1']+I[X_1+X_2:X_1'+X_2\mid X_1+X_2+X_1'+X_2']=2k.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record