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

1 topic

2 results

Clear filters
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