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

Alice pr le

alice_pr_le

Plain-language statement

Honest Alice has error ≥ e with probability ≤ q

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.8.0

Alice steps cost

alice_steps_cost

Plain-language statement

Alice makes few queries, regardless of Bob and Vera

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.8.0

Alices close

alices_close

Plain-language statement

Alice produces (p,y) with p close to o.probs y with good probability

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.8.0

Alices success

alices_success

Plain-language statement

Alice produces (p,y) with p close and y true with good probability, since if we condition on Alice being close she does as least as well as a close oracle.

probabilitycomplexity theoryinteractive protocols

Source project: debate

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Approx hom pfr

approx_hom_pfr

Project documentation

An approximate-homomorphism theorem for finite elementary abelian 22-groups. Let f:GGf:G\to G' and K>0K>0. If at least a proportion K1K^{-1} of pairs (x,y)G2(x,y)\in G^2 satisfy f(x+y)=f(x)+f(y)f(x+y)=f(x)+f(y), then there are an additive homomorphism φ:GG\varphi:G\to G' and a constant cGc\in G' such that f(x)=φ(x)+cf(x)=\varphi(x)+c for at least G/(2144K122)|G|/(2^{144}K^{122}) values of xx.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture

Plain-language statement

If AF2nA \subset {\bf F}_2^n is finite non-empty with A+AKA|A+A| \leq K|A|, then there exists a subgroup HH of F2n{\bf F}_2^n with HA|H| \leq |A| such that AA can be covered by at most 2K92K^9 translates of HH.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record