OAI/Analysis/LipschitzHilbert/Fourier/ModulatedInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joint parameter dependence and a uniform bound for the separated frequency multiplier. These are used to interchange its parameter and physical-space integrals.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedFrequency_eq_window line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverse_modulated_frequency line 25
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.modulated_inverse_joint_continuous line 33
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverse_norm_le line 40
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.modulated_inverse_norm_le line 47