OAI/Analysis/LipschitzHilbert/Estimates/FiniteUnitAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the outside Fourier weight to the whole finite convolution sum. The number of rows never appears in the transferred bound.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.finite_unit_convolution_average_bound line 12