OAI/Analysis/LipschitzHilbert/Estimates/FiniteUnitAverageL1.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_l1 line 12