OAI/Analysis/LipschitzHilbert/Fourier/SchwartzBandPrimitive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual primitive of an annular Schwartz packet. The Fourier quotient is smooth because the packet vanishes near frequency zero.

  1. theorem OAI.LipschitzHilbert.derivative_coefficient_ne_zero line 15
  2. theorem OAI.LipschitzHilbert.exists_schwartz_band_primitive line 21
  3. theorem OAI.LipschitzHilbert.schwartz_primitive_energy line 78