OAI/Analysis/LipschitzHilbert/Fourier/L1MultiplierLinearity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact finite input and test reconstruction for frequency multipliers with an integrable envelope.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.planarFourier_finset_sum_l1 line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.variableFrequencyMultiplier_finset_sum_l1 line 25
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.variableFrequencyMultiplier_pairing_finset_sum_l1 line 37
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.planarFourier_real_smul_l1 line 58
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.variableFrequencyMultiplier_real_smul_l1 line 64
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.variableFrequencyMultiplier_pairing_real_smul_l1 line 72