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, , , and every truncated Calderón-Zygmund operator has the required uniform strong bound. Then the two-sided metric Carleson operator is bounded from Lorentz to weak Lorentz , with the explicit project constant .
harmonic analysisFourier analysismeasure theory
Source project: Carleson formalization
Person-level attribution pending.