OAI/Analysis/LipschitzHilbert/Fourier/AnnularPositiveCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The positive half of the geometric low-pass difference is Schwartz and is exactly covered by a fixed admissible enlarged cutoff.

  1. def OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifferenceSchwartz line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifferenceSchwartz_apply line 16
  3. def OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_apply line 22
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_active line 27
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_support line 41
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_enlarged line 45
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_real line 52
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_real line 55
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_even line 60