OAI/Analysis/LipschitzHilbert/Packets/NormalizedPacketProfiles.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A single Fourier parameter determines both normalized wave profiles. Their common bound is chosen before all spatial scales and frequency bins.

  1. def OAI.LipschitzHilbert.PacketRepresentation.synthesisProfile line 10
  2. def OAI.LipschitzHilbert.PacketRepresentation.analysisProfile line 13
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.synthesisProfile_eq line 17
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.analysisProfile_eq line 26
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.uniform_normalized_profile_pair line 36
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.physical_synthesisProfile line 52
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.physical_analysisProfile line 61