OAI/Analysis/LipschitzHilbert/Estimates/DyadicSmoothEmbedding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth projection Carleson coefficients in the finite product embedding. The low-pass majorant is allowed to hold almost everywhere.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadic_smooth_product_embedding line 14