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

1 topic

167 results

Clear filters
Project-declaredLean 4.8.0

Oracle fold succ prob

Oracle.fold_succ_prob

Plain-language statement

(o.fold (n+1)).prob y decomposes as a product

probabilitycomplexity theoryinteractive protocols

Source project: debate

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
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.8.0

PMF integrable of support finite

PMF.integrable_of_support_finite

Plain-language statement

Everything is integrable over PMFs with finite support

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record