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

1 topic

130 results

Clear filters
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 δ>0\delta>0 and every measure tolerance ε>0\varepsilon>0, one can choose N0N_0 so that the set where supN>N0f(x)FN(x)\sup_{N>N_0}\lVert f(x)-F_N(x)\rVert exceeds δ\delta has measure at most ε\varepsilon. Then FN(x)F_N(x) converges to f(x)f(x) for almost every xx.

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 A\mathfrak{A} of pairwise incomparable tiles, and measurable functions ff and gg bounded by the indicators of FF and GG, the pairing of gg with the Carleson sum over A\mathfrak{A} is controlled by the L2L^2 norms of ff and gg and by positive powers of the two tile-density parameters. Concretely, the bound is

C(a,q)dens1(A)(q1)/(8a4)dens2(A)1/q1/2f2g2.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 A\mathfrak A, a measurable set AGA\subseteq G, and measurable ff bounded by 1F\mathbf 1_F, the norm of the Carleson sum has the integral estimate

A+CarlesonSumAf(x)dxC(a,q)dens1(A)(q1)/(8a4)dens2(A)1/q1/2f2μ(G)1/2.\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 NN, and a spatial grid cube LL. Among the auxiliary tiles attached to an antichain A\mathfrak{A} whose spatial cube is exactly LL, the total measure of their active sets inside GG is at most

2a(N+5)dens1(A)μ(L).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 uu, the union of the grid cubes in its level-nn boundary family has measure at most a constant C(X,n)C(X,n) times the measure of the spatial cube I(u)\mathcal{I}(u).

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record