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

All topics

38 results

Clear filters
Project-declaredLean 4.32.0

Mem arc Set iff nnnorm width

BohrSet.mem_arcSet_iff_nnnorm_width

Plain-language statement

A point xx belongs to the arc model of a Bohr set BB exactly when every frequency ψ\psi of BB satisfies angle(ψ(x),1)widthB(ψ)\|\operatorname{angle}(\psi(x),1)\|\le \operatorname{width}_B(\psi). Thus membership can be checked using only the stored frequencies and widths.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Mem chord Set iff nnnorm width

BohrSet.mem_chordSet_iff_nnnorm_width

Plain-language statement

A point xx belongs to the chord model of a Bohr set BB exactly when 1ψ(x)widthB(ψ)\|1-\psi(x)\|\le \operatorname{width}_B(\psi) for every frequency ψ\psi of BB.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Chang

chang

Project documentation

Chang's lemma for the large Fourier spectrum. If ff is nonzero and η>0\eta>0, there is a subset Δ\Delta of the η\eta-large spectrum such that the entire large spectrum lies in the additive span of Δ\Delta. The theorem also gives the explicit bound ΔCeL ⁣(f12/(f22G))/η2|\Delta| \le \left\lceil C e\,\left\lceil \mathcal L\!\left(\|f\|_1^2/(\|f\|_2^2|G|)\right)\right\rceil/\eta^2\right\rceil, with the project's constant CC.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

C Lp Norm conv le c Lp Norm dconv

cLpNorm_conv_le_cLpNorm_dconv

Plain-language statement

For a complex-valued function on the ambient finite group and a nonzero even integer nn, ordinary self-convolution has no larger normalized LnL^n norm than self-difference-convolution: ffnffn\|f*f\|_n\le\|f\mathbin{\circleddash}f\|_n.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

C Lp Norm dft indicator one pow

cLpNorm_dft_indicator_one_pow

Plain-language statement

The 2n2n-th Fourier moment of the indicator of a finite set equals its order-nn additive energy: 1s^2n2n=En(s)\|\widehat{1_s}\|_{2n}^{2n}=E_n(s). This is the standard bridge between Fourier norms and additive tuple counts.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Di in ff

di_in_ff

Project documentation

A finite-field density-increment lemma. If the normalized additive correlation of AA with a set CC of density at least γ\gamma differs from its random value by at least ε\varepsilon, then there is a subspace VV of explicitly bounded codimension. Averaging 1A1_A over VV raises its LL^\infty density to at least (1+ε/32)α(1+\varepsilon/32)\alpha, where α\alpha is the density of AA.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record