OAI/Analysis/LipschitzHilbert/Fourier/ShortPositiveConvolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Short-scale convolution control by the sum of the actual source functions before integration. This avoids a factor counting the scales.

  1. theorem OAI.LipschitzHilbert.short_positiveConvolution_integral line 16