OAI/Analysis/LipschitzHilbert/Estimates/SmoothCarlesonEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth Carleson product estimate on every finite frequency range. The countable spatial partition introduces no constant or cutoff.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.smooth_carleson_estimate line 13