Oracle fold succ prob
Oracle.fold_succ_prob
Plain-language statement
(o.fold (n+1)).prob y decomposes as a product
Source project: debate
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 167 research declarations. Search 10,000 more complete Mathlib declarations.
167 results
Clear filtersOracle.fold_succ_prob
Plain-language statement
(o.fold (n+1)).prob y decomposes as a product
Source project: debate
Person-level attribution pending.
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|.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
PFR_conjecture_improv
Project documentation
Improved polynomial Freiman-Ruzsa theorem. Let be a nonempty subset of a finite elementary abelian -group. If , then there are a subspace and a set of representatives such that , , and .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
PFR_conjecture_improv'
Project documentation
Improved polynomial Freiman-Ruzsa theorem without a finite ambient-group assumption. Let be a nonempty finite subset of an elementary abelian -group. If , then there are a finite subspace and a finite set such that , , and .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
PFR_conjecture'
Project documentation
Polynomial Freiman-Ruzsa theorem without a finite ambient-group assumption. Let be a nonempty finite subset of an elementary abelian -group. If , then there are a finite subspace and a finite set such that , , and .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
PMF.integrable_of_support_finite
Plain-language statement
Everything is integrable over PMFs with finite support
Source project: debate
Person-level attribution pending.