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

1 topic

5 results

Clear filters
Project-declaredLean 4.32.0

EnumΘ'Arg Max eq iff

enumΘ'ArgMax_eq_iff

Plain-language statement

Among the first n+1n+1 enumerated phases, enumΘ'ArgMax returns the smallest index ii at which the function gg attains its maximum at xx. Equivalently, every index jnj\le n has value at most the value at ii, and every earlier index j<ij<i has strictly smaller value.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Metric carleson

metric_carleson

Plain-language statement

Let 1<q21 < q \le 2 and let qq' be its Hölder conjugate. In the project’s cancellative metric-space setting, assume the associated nontangential operators satisfy the required uniform L2L^2 bound. If FF and GG are measurable and ff is measurable with f(x)1F(x)\lVert f(x)\rVert \le \mathbf{1}_F(x), then the Carleson operator obeys the restricted estimate

G+CKf(x)dxC(a,q)μ(G)1/qμ(F)1/q.\int_G^+ \mathcal{C}_K f(x)\,dx \le C(a,q)\,\mu(G)^{1/q'}\mu(F)^{1/q}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

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

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