fpvandoorn/carleson

Technical evidence

Versions, dependency locks, and provider build observations for Carleson formalization. The project page remains the canonical scholarly record.

101 GitHub starsApache-2.038 indexed versionsRepository Homepage

Therefore source index

Exact indexed revision

74ef907d6bdb60797b88655bc16e3032fb835fdc

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

External build observation

Exact commit and toolchain

No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.

Pin this exact source in lakefile.lean

require carleson from git "https://github.com/fpvandoorn/carleson.git" @ "74ef907d6bdb60797b88655bc16e3032fb835fdc"

Dependency graph

2 direct, 8 transitive

Direct dependencies

checkdecls

3d425859e73fcfbef85b9638c2a91708ef4a22d4

git

mathlib

81a5d257c8e410db227a6665ed08f64fea08e997

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

38 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 38 versions

0.0.0Indexed

74ef907d6bdb60797b88655bc16e3032fb835fdc

leanprover/lean4:v4.32.0

10 dependencies · 23 Jul 2026

v4.32.0

c82b9f685d43c9c35ceddcc89fdb97eee0482ff3

leanprover/lean4:v4.32.0

10 dependencies · 16 Jul 2026

v4.31.0

c19427808277b740c69b1e1146e636a3b20b73c4

leanprover/lean4:v4.31.0

10 dependencies · 14 Jul 2026

v4.30.0-rc2

7a0ea9d6d5bf3f51a44b195d3bbb43a0519f6eea

leanprover/lean4:v4.30.0-rc2

10 dependencies · 30 Apr 2026

v4.29.1

17be9be73343aefe5a124e0fac9d2aebb08e6759

leanprover/lean4:v4.29.1

10 dependencies · 26 Apr 2026

v4.29.0

306ae5b29300771aece1aa39f0a939183cc59486

leanprover/lean4:v4.29.0

10 dependencies · 26 Apr 2026

v4.28.0

fa053d35964457f6e660b230781a5112940c5d22

leanprover/lean4:v4.28.0

10 dependencies · 18 Feb 2026

v4.28.0-rc1

70dfd02d7e46adb4be4d9343d7e7fa053dc5aac1

leanprover/lean4:v4.28.0-rc1

10 dependencies · 26 Jan 2026

v4.27.0

0ddd15b3b35b21a6ae175011f02fda5d1a0abd69

leanprover/lean4:v4.27.0

10 dependencies · 24 Jan 2026

v4.27.0-rc1

8ac3da8b5c31efc2246329fa44adad67950b733a

leanprover/lean4:v4.27.0-rc1

10 dependencies · 17 Dec 2025

v4.26.0

068f68eacb9956ce5dcfb0b85e74423bb1338ab3

leanprover/lean4:v4.26.0

10 dependencies · 15 Dec 2025

v4.25.0

e521e4a21da60cf720c3897c2574c0592d6c1870

leanprover/lean4:v4.25.0

10 dependencies · 17 Nov 2025

v4.25.0-rc2

e307a2c1f65d10ad17ad841cbf4d572ab32b2cd0

leanprover/lean4:v4.25.0-rc2

10 dependencies · 30 Oct 2025

v4.24.0

5441a784bb4919642e8eb6c56b6af3b21cffd3f5

leanprover/lean4:v4.24.0

10 dependencies · 16 Oct 2025

v4.23.0-rc2

e5f273f19a890a3217015b5beb2c6ced50889444

leanprover/lean4:v4.23.0-rc2

10 dependencies · 19 Aug 2025

v4.22.0

4ae1b9453d51b3107e7dd677e423d7c2edf2582c

leanprover/lean4:v4.22.0

10 dependencies · 19 Aug 2025

v4.22.0-rc4

7192b7e862fba272c30b677a96b82d5b7bc43837

leanprover/lean4:v4.22.0-rc4

10 dependencies · 24 Jul 2025

v4.22.0-rc3

5fce53bd9e9a98533a5b628bc73dbff1b5fbb2f9

leanprover/lean4:v4.22.0-rc3

10 dependencies · 15 Jul 2025

v4.22.0-rc2

d5b5f1844032be212910e79d625b9df0529e7f89

leanprover/lean4:v4.22.0-rc2

10 dependencies · 2 Jul 2025

v4.21.0

f621ab450c2447633a013603d32950a77f3e4649

leanprover/lean4:v4.21.0

10 dependencies · 1 Jul 2025

v4.21.0-rc3

6512b424f2e718d58f19a1e2b2e4e6b6717470c9

leanprover/lean4:v4.21.0-rc3

10 dependencies · 8 Jun 2025

v4.20.0

95d25d8ab9879ef633277143c36a6d82469061d2

leanprover/lean4:v4.20.0

10 dependencies · 2 Jun 2025

v4.20.0-rc5

38af1a3e236103f3e43fbe7b8176416302c79159

leanprover/lean4:v4.20.0-rc5

10 dependencies · 27 May 2025

v4.20.0-rc4

608e5423337d3ffb9f2c9591ace39a3f1935cfe5

leanprover/lean4:v4.20.0-rc4

10 dependencies · 7 May 2025

v4.20.0-rc2

7e68f44cdd13e07368eb8814e372a5160b012091

leanprover/lean4:v4.20.0-rc2

10 dependencies · 5 May 2025

v4.19.0

b753be0fb4bc19883b5379e57f0c1a33774975ea

leanprover/lean4:v4.19.0

10 dependencies · 2 May 2025

v4.19.0-rc3

f69820f53436b764bbc6b2ba26070a6becdce0be

leanprover/lean4:v4.19.0-rc3

10 dependencies · 14 Apr 2025

v4.19.0-rc2

596e40748eb59deb1cd6229204f84c13360bb7f3

leanprover/lean4:v4.19.0-rc2

10 dependencies · 12 Apr 2025

v4.18.0

841c1e8343974e0d886dfb572232a90a71a3901a

leanprover/lean4:v4.18.0

10 dependencies · 1 Apr 2025

v4.18.0-rc1

4792cda0108cd8a46a3006d935d1142d2631e3bf

leanprover/lean4:v4.18.0-rc1

10 dependencies · 6 Mar 2025

v4.17.0

f4c28795c8b5882a117ca133debd9f1387da463f

leanprover/lean4:v4.17.0

10 dependencies · 4 Mar 2025

v4.17.0-rc1

5894b593ab4473d3e95c8d7b5d93a99cbfd0e2b7

leanprover/lean4:v4.17.0-rc1

10 dependencies · 10 Feb 2025

v4.16.0

a5d265f109105809de4aaff16776b7c16b1c0bd5

leanprover/lean4:v4.16.0

10 dependencies · 7 Feb 2025

v4.16.0-rc2

c4593b3f98a621dae9361b03867e8a07e5baeaea

leanprover/lean4:v4.16.0-rc2

10 dependencies · 14 Jan 2025

v4.15.0

386a3c6e178f3c1b92ad5547a69b48ebfe1564ea

leanprover/lean4:v4.15.0

10 dependencies · 6 Jan 2025

v4.14.0-rc2

0ba357e18157bf100b8445ab919c150a56acb83e

leanprover/lean4:v4.14.0-rc2

10 dependencies · 21 Nov 2024

v4.13.0

0f438e4aecebdc2d592b05519666bcbc404e1efc

leanprover/lean4:v4.13.0

14 dependencies · 10 Nov 2024

v4.12.0

9001fa286ce1ea2b25531f06d8ec8f5dfab21a26

leanprover/lean4:v4.12.0

13 dependencies · 4 Oct 2024

Version	Revision	Toolchain	Dependencies	Date
0.0.0Indexed	74ef907d6bdb	leanprover/lean4:v4.32.0	10	23 Jul 2026
v4.32.0	c82b9f685d43	leanprover/lean4:v4.32.0	10	16 Jul 2026
v4.31.0	c19427808277	leanprover/lean4:v4.31.0	10	14 Jul 2026
v4.30.0-rc2	7a0ea9d6d5bf	leanprover/lean4:v4.30.0-rc2	10	30 Apr 2026
v4.29.1	17be9be73343	leanprover/lean4:v4.29.1	10	26 Apr 2026
v4.29.0	306ae5b29300	leanprover/lean4:v4.29.0	10	26 Apr 2026
v4.28.0	fa053d359644	leanprover/lean4:v4.28.0	10	18 Feb 2026
v4.28.0-rc1	70dfd02d7e46	leanprover/lean4:v4.28.0-rc1	10	26 Jan 2026
v4.27.0	0ddd15b3b35b	leanprover/lean4:v4.27.0	10	24 Jan 2026
v4.27.0-rc1	8ac3da8b5c31	leanprover/lean4:v4.27.0-rc1	10	17 Dec 2025
v4.26.0	068f68eacb99	leanprover/lean4:v4.26.0	10	15 Dec 2025
v4.25.0	e521e4a21da6	leanprover/lean4:v4.25.0	10	17 Nov 2025
v4.25.0-rc2	e307a2c1f65d	leanprover/lean4:v4.25.0-rc2	10	30 Oct 2025
v4.24.0	5441a784bb49	leanprover/lean4:v4.24.0	10	16 Oct 2025
v4.23.0-rc2	e5f273f19a89	leanprover/lean4:v4.23.0-rc2	10	19 Aug 2025
v4.22.0	4ae1b9453d51	leanprover/lean4:v4.22.0	10	19 Aug 2025
v4.22.0-rc4	7192b7e862fb	leanprover/lean4:v4.22.0-rc4	10	24 Jul 2025
v4.22.0-rc3	5fce53bd9e9a	leanprover/lean4:v4.22.0-rc3	10	15 Jul 2025
v4.22.0-rc2	d5b5f1844032	leanprover/lean4:v4.22.0-rc2	10	2 Jul 2025
v4.21.0	f621ab450c24	leanprover/lean4:v4.21.0	10	1 Jul 2025
v4.21.0-rc3	6512b424f2e7	leanprover/lean4:v4.21.0-rc3	10	8 Jun 2025
v4.20.0	95d25d8ab987	leanprover/lean4:v4.20.0	10	2 Jun 2025
v4.20.0-rc5	38af1a3e2361	leanprover/lean4:v4.20.0-rc5	10	27 May 2025
v4.20.0-rc4	608e5423337d	leanprover/lean4:v4.20.0-rc4	10	7 May 2025
v4.20.0-rc2	7e68f44cdd13	leanprover/lean4:v4.20.0-rc2	10	5 May 2025
v4.19.0	b753be0fb4bc	leanprover/lean4:v4.19.0	10	2 May 2025
v4.19.0-rc3	f69820f53436	leanprover/lean4:v4.19.0-rc3	10	14 Apr 2025
v4.19.0-rc2	596e40748eb5	leanprover/lean4:v4.19.0-rc2	10	12 Apr 2025
v4.18.0	841c1e834397	leanprover/lean4:v4.18.0	10	1 Apr 2025
v4.18.0-rc1	4792cda0108c	leanprover/lean4:v4.18.0-rc1	10	6 Mar 2025
v4.17.0	f4c28795c8b5	leanprover/lean4:v4.17.0	10	4 Mar 2025
v4.17.0-rc1	5894b593ab44	leanprover/lean4:v4.17.0-rc1	10	10 Feb 2025
v4.16.0	a5d265f10910	leanprover/lean4:v4.16.0	10	7 Feb 2025
v4.16.0-rc2	c4593b3f98a6	leanprover/lean4:v4.16.0-rc2	10	14 Jan 2025
v4.15.0	386a3c6e178f	leanprover/lean4:v4.15.0	10	6 Jan 2025
v4.14.0-rc2	0ba357e18157	leanprover/lean4:v4.14.0-rc2	10	21 Nov 2024
v4.13.0	0f438e4aeceb	leanprover/lean4:v4.13.0	14	10 Nov 2024
v4.12.0	9001fa286ce1	leanprover/lean4:v4.12.0	13	4 Oct 2024

Build history

1 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

Selected source declarations

Selected declarations

Search within package

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

Project-declaredLean 4.32.0

Adjoint Carleson adjoint

adjointCarleson_adjoint

Plain-language statement

adjointCarleson is the adjoint of carlesonOn.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Ae tendsto zero of distribution le

ae_tendsto_zero_of_distribution_le

Plain-language statement

Suppose that, for every error threshold $\delta>0$ and every measure tolerance $\varepsilon>0$ , one can choose $N_0$ so that the set where $\sup_{N>N_0}\lVert f(x)-F_N(x)\rVert$ exceeds $\delta$ has measure at most $\varepsilon$ . Then $F_N(x)$ converges to $f(x)$ for almost every $x$ .

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Antichain operator

antichain_operator

Plain-language statement

For an antichain $\mathfrak{A}$ of pairwise incomparable tiles, and measurable functions $f$ and $g$ bounded by the indicators of $F$ and $G$ , the pairing of $g$ with the Carleson sum over $\mathfrak{A}$ is controlled by the $L^2$ norms of $f$ and $g$ and by positive powers of the two tile-density parameters. Concretely, the bound is

$C(a,q)\,\mathrm{dens}_1(\mathfrak{A})^{(q-1)/(8a^4)}\,\mathrm{dens}_2(\mathfrak{A})^{1/q-1/2}\,\lVert f\rVert_2\lVert g\rVert_2.$

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Antichain operator

antichain_operator'

Plain-language statement

For an antichain $\mathfrak A$ , a measurable set $A\subseteq G$ , and measurable $f$ bounded by $\mathbf 1_F$ , the norm of the Carleson sum has the integral estimate

$\int_A^+\lVert\operatorname{CarlesonSum}_{\mathfrak A}f(x)\rVert\,dx\le C(a,q)\,\mathrm{dens}_1(\mathfrak A)^{(q-1)/(8a^4)}\,\mathrm{dens}_2(\mathfrak A)^{1/q-1/2}\,\lVert f\rVert_2\,\mu(G)^{1/2}.$

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Stack density

Antichain.stack_density

Plain-language statement

Fix a frequency parameter $\vartheta$ , a level $N$ , and a spatial grid cube $L$ . Among the auxiliary tiles attached to an antichain $\mathfrak{A}$ whose spatial cube is exactly $L$ , the total measure of their active sets inside $G$ is at most

$2^{a(N+5)}\,\mathrm{dens}_1(\mathfrak{A})\,\mu(L).$

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Boundary exception

boundary_exception

Plain-language statement

For a tile $u$ , the union of the grid cubes in its level- $n$ boundary family has measure at most a constant $C(X,n)$ times the measure of the spatial cube $\mathcal{I}(u)$ .

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record