Torsion free doubling
torsion_free_doubling
Plain-language statement
If G is torsion-free and X, Y are G-valued random variables then d[X; 2Y] ≤ 5d[X; Y].
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
Source-pinned research
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.
45 results
Clear filterstorsion_free_doubling
Plain-language statement
If G is torsion-free and X, Y are G-valued random variables then d[X; 2Y] ≤ 5d[X; Y].
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
torsion_PFR
Project documentation
Polynomial Freiman-Ruzsa theorem for bounded-torsion groups. Let be a finite abelian group in which for every , with . If is nonempty and , then there are a subgroup and a set such that , , and .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
weak_PFR_asymm_prelim
Plain-language statement
An asymmetric weak-PFR estimate. Let be nonempty finite subsets of a rank- free -module . There are a subgroup , cosets , and nonempty fibers and such that and
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.