OAI/Analysis/LipschitzHilbert/Fourier/FiniteSeparatedSymbolBoundL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer a uniform bound on the complete separated convolution sum to the original finite symbol pairing. The two exact interchanges are already proved, so no sum of individual row bounds is introduced.

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