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

Two sided metric carleson has Lorentz Type

two_sided_metric_carleson_hasLorentzType

Plain-language statement

Assume the phase space is countable, a4a\ge4, 1<q<21<q<2, and every truncated Calderón-Zygmund operator TrT_r has the required uniform strong L2L^2 bound. Then the two-sided metric Carleson operator is bounded from Lorentz Lq,1L^{q,1} to weak Lorentz Lq,L^{q,\infty}, with the explicit project constant 4C(a,q)/q4C(a,q)/q.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record