OAI/Analysis/LipschitzHilbert/Fourier/VerticalInverseMultiplier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact inverse-frequency representation of vertical convolution.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.vertical_inverse_multiplier line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_vertical_multiplier line 58