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 83 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

83 results

Clear filters
Project-declaredLean 4.33.0-rc1

Multi Dist of cast

multiDist_of_cast

Plain-language statement

Multidistance is unchanged when a finite family of random variables is reindexed along an equality m=mm'=m. This says that the quantity depends on the family, not on the particular equal presentation of its finite index type.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Multidist ruzsa IV

multidist_ruzsa_IV

Project documentation

Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Let W := ∑ X_i. Then d[W;-W] ≤ 2 D[X_i].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Multi Tau min sum le

multiTau_min_sum_le

Plain-language statement

If (Xi)1im(X_i)_{1 \leq i \leq m} is a τ\tau-minimizer, then i=1md[Xi;X0]2mηd[X0;X0]\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0].

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

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