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

1 topic
Project-declaredLean 4.32.0

S truncation

S_truncation

Plain-language statement

Let 1<q21<q\le2, let qq' be its Hölder conjugate, and suppose the linearized nontangential operators have the required uniform L2L^2 bound. For bounded measurable F,GF,G and measurable ff with f(x)1F(x)\lVert f(x)\rVert\le\mathbf 1_F(x), the supremum over all truncated scale intervals Bs1s2B-B\le s_1\le s_2\le B satisfies

G+sups1s2Ts1,s2f(x)dxC(a,q)μ(G)1/qμ(F)1/q.\int_G^+\sup_{s_1\le s_2}\lVert T_{s_1,s_2}f(x)\rVert\,dx\le C(a,q)\,\mu(G)^{1/q'}\mu(F)^{1/q}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record