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

1 topic

3 results

Clear filters
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

Card of dual constrained

card_of_dual_constrained

Plain-language statement

In the ambient finite F2\mathbb F_2-vector space, exactly half of the additive homomorphisms φ:GF2\varphi:G\to\mathbb F_2 take a fixed nonzero vector xx to 11: 2{φ:φ(x)=1}=G2\,|\{\varphi:\varphi(x)=1\}|=|G|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Card of slice

card_of_slice

Plain-language statement

For every set AA in the ambient finite F2\mathbb F_2-vector space, some linear functional φ:GF2\varphi:G\to\mathbb F_2 has at least (A1)/2(|A|-1)/2 elements of AA in its 11-fiber.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record