therefore
Sign up
Open navigation
Canonical project page

YaelDillies/APAP

Technical evidence

Versions, dependency locks, and provider build observations for Arithmetic Progressions Almost Periodicity. The project page remains the canonical scholarly record.

27 GitHub starsApache-2.021 indexed versionsRepositoryHomepage
mathcombinatoricsadditive-combinatoricsfourier-analysis

Therefore source index

Exact indexed revision

afafc42a5326d770d0f853f060b2f63947c13f0f

Toolchain
leanprover/lean4:v4.32.0
Tag
v4.32.0
Declarations
38
Mathlib revision
81a5d257c8e4

External build observation

Exact commit and toolchain

Reservoir observed a successful build of commit afafc42a5326 with leanprover/lean4:v4.32.0 on 20 Jul 2026. Therefore did not run this build.

Reservoir build log

Pin this exact source in lakefile.lean

require APAP from git "https://github.com/YaelDillies/apap.git" @ "afafc42a5326d770d0f853f060b2f63947c13f0f"

Dependency graph

3 direct, 8 transitive

Direct dependencies

mathlib

81a5d257c8e410db227a6665ed08f64fea08e997

git
AddCombi

8ab39477ca274ffc4600eb4eb36c70988d59ccda

git
checkdecls

3d425859e73fcfbef85b9638c2a91708ef4a22d4

git
Transitive dependencies

Resolved through the exact indexed manifest.

leanprover-community/plausible

e12c1910fe855cbfc38803cd4e55543906d5fa62

git
leanprover-community/LeanSearchClient

c5d5b8fe6e5158def25cd28eb94e4141ad97c843

git
leanprover-community/importGraph

7e9612bf0b9ee66db3cb5b9988a35afc706f5a12

git
leanprover-community/proofwidgets

6e311e2a844da9b2cc3971187df2fe0066947b93

git
leanprover-community/aesop

a7dbf0c63b694e47f425f3dcddbc0e178bb432d3

git
leanprover-community/Qq

38d591e778f100aec9762bb582f9c7f55f50e9dc

git
leanprover-community/batteries

023ce7d62a0531e22a5331e20b587817a80d49ff

git
leanprover/Cli

88679d088c9720c27ebdf2ba4dafe17341747f94

git

Version history

21 Reservoir versions

Version records come from the cached Reservoir snapshot. The highlighted row is the exact revision used for Therefore's declaration index.

Show all 21 versions
v4.32.0Indexed

afafc42a5326d770d0f853f060b2f63947c13f0f

leanprover/lean4:v4.32.0

11 dependencies · 16 Jul 2026

v4.32.0-rc1

c1d84416f68bb14a4ada9b79f284a0478c6f0bf5

leanprover/lean4:v4.32.0-rc1

11 dependencies · 3 Jul 2026

v4.31.0

86a7ccbaaef3ef5a25a6d2428965671b078622ab

leanprover/lean4:v4.31.0

11 dependencies · 16 Jun 2026

v4.30.0

8e39fdc67497efbcf1f7401080079005ff035767

leanprover/lean4:v4.30.0

11 dependencies · 30 May 2026

v4.30.0-rc2

1d8e97fdb207f2875b8caea1373fed0aee2dd86c

leanprover/lean4:v4.30.0-rc2

11 dependencies · 4 May 2026

v4.29.0

2daecd94615de96851d9124a8c095b6469a0426e

leanprover/lean4:v4.29.0

10 dependencies · 1 Apr 2026

v4.28.0

eba2c2b0e8309e19de76037c188dc14899729bce

leanprover/lean4:v4.28.0

10 dependencies · 11 Mar 2026

v4.28.0-rc1

5db8083bb6801e7c9238cc0837e763d2530ae789

leanprover/lean4:v4.28.0-rc1

10 dependencies · 9 Feb 2026

v4.27.0

96167d24d9724269561f5f1ed7d29d779157e4da

leanprover/lean4:v4.27.0

10 dependencies · 24 Jan 2026

v4.27.0-rc1

96325adf1d139b2adaa32d9839f096eec959480d

leanprover/lean4:v4.27.0-rc1

10 dependencies · 24 Dec 2025

v4.26.0

d3e4b6a8bd62e86ca2ded6547abdc930c3cd0952

leanprover/lean4:v4.26.0

10 dependencies · 14 Dec 2025

v4.26.0-rc2

33f13f9492ac44287719323c6260f760298c9915

leanprover/lean4:v4.26.0-rc2

10 dependencies · 29 Nov 2025

v4.25.0

5bbd91f52aa2e2d413a19afc10d30362e4872527

leanprover/lean4:v4.25.0

9 dependencies · 16 Nov 2025

v4.24.0

aa9029c877257387fa57b1dec9db15a0bbb71ed0

leanprover/lean4:v4.24.0

9 dependencies · 14 Oct 2025

v4.23.0

433ca602181a3e2497ddbe8d0cc7454b3b817f9c

leanprover/lean4:v4.23.0

9 dependencies · 14 Oct 2025

v4.22.0

44d47c5733bac290a2f3e87bd529128007911772

leanprover/lean4:v4.22.0

9 dependencies · 19 Aug 2025

v4.21.0

650be762dce986bf848a7b3a8f291aaf496dbbb5

leanprover/lean4:v4.21.0

9 dependencies · 30 Jun 2025

v4.20.1

4b2c5ca3a4fbd89629e42e100e52dcb22c41b032

leanprover/lean4:v4.20.1

9 dependencies · 6 Jun 2025

v4.19.0

61769c82c1a8e2efd65da4490925180c54a611a7

leanprover/lean4:v4.19.0

9 dependencies · 2 May 2025

v4.18.0

9a8fb1552da10e6b6ebc836b75c990c7793cf1f2

leanprover/lean4:v4.18.0

9 dependencies · 4 Apr 2025

v4.17.0

576332487fed66af7f4b9ca474c0984c5ed04c8b

leanprover/lean4:v4.17.0

9 dependencies · 5 Mar 2025

Build history

4 observations for the indexed commit

These are Reservoir provider observations. They never change a Therefore proof status and they are not independent rebuilds by Therefore.

Show provider build history

leanprover/lean4:v4.32.1

Build failed · Test not observed · 23 Jul 2026

Build log

leanprover/lean4:v4.32.0

Build passed · Test not observed · 20 Jul 2026

Build log

leanprover/lean4:v4.33.0-rc1

Build failed · Test not observed · 19 Jul 2026

Build log

leanprover/lean4:v4.32.0

Build passed · Test not observed · 17 Jul 2026

Build log

Selected source declarations

Selected declarations

Search within package

Showing 6 of 17 source-indexed declarations. The canonical project page and project search expose the full index.

Project-declaredLean 4.32.0

Add Dissociated boring Energy le

AddDissociated.boringEnergy_le

Project documentation

If a finite set ss is additively dissociated, then its order-nn additive energy is at most Cnnn∣s∣nC^n n^n |s|^n, where CC is the project's Chang constant. This is the quantitative dissociated-set estimate used in the proof of Chang's lemma.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Linfty almost periodicity

AlmostPeriodicity.linfty_almost_periodicity

Project documentation

An L∞L^\infty almost-periodicity theorem. Under the small-growth hypothesis σ[A,S]≤K\sigma[A,S]\le K, and for nonempty finite sets B,CB,C, there is a set of translations TT with ∣T∣≥K−4096⌈L(∣C∣/∣B∣)⌉/ε2∣S∣|T|\ge K^{-4096\lceil\mathcal L(|C|/|B|)\rceil/\varepsilon^2}|S|. Every t∈Tt\in T changes the normalized convolution μA∗1B∗μC\mu_A*1_B*\mu_C by at most ε\varepsilon in L∞L^\infty.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Linfty almost periodicity boosted

AlmostPeriodicity.linfty_almost_periodicity_boosted

Plain-language statement

A boosted L∞L^\infty almost-periodicity estimate. Under σ[A,S]≤K\sigma[A,S]\le K, it finds a large set TT, with the stated lower bound ∣T∣≥K−4096⌈L(∣C∣/∣B∣)⌉k2/ε2∣S∣|T|\ge K^{-4096\lceil\mathcal L(|C|/|B|)\rceil k^2/\varepsilon^2}|S|, such that averaging the target convolution against the kk-fold convolution of μT\mu_T changes it by at most ε\varepsilon in L∞L^\infty.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Ap in ff

ap_in_ff

Project documentation

A finite-field approximation lemma. If A1A_1 and A2A_2 each have density at least α\alpha, then for any test set SS and 0<ε≤10<\varepsilon\le1 there is a subspace VV of explicitly bounded codimension such that smoothing μA1∗μA2\mu_{A_1}*\mu_{A_2} by the uniform measure on VV changes its total mass on SS by at most ε\varepsilon.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Chord Set subset smul arc Set

BohrSet.chordSet_subset_smul_arcSet

Plain-language statement

For a finite ambient group, the chord model of a Bohr set BB is contained in the arc model after widening BB by the factor π/2\pi/2: Bchord⊆((π/2)B)arcB_{\mathrm{chord}}\subseteq ((\pi/2)B)_{\mathrm{arc}}.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Le iff width

BohrSet.le_iff_width

Plain-language statement

Characterization of the order on Bohr sets. The relation B1≤B2B_1\le B_2 holds exactly when every frequency of B2B_2 is also a frequency of B1B_1, and width⁡B1(ψ)≤width⁡B2(ψ)\operatorname{width}_{B_1}(\psi)\le \operatorname{width}_{B_2}(\psi) for each such frequency.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record