OAI/Analysis/LipschitzHilbert/Packets/AnalyzingProfileNormalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The analyzing wave uses reflection and conjugation together. Its positive carrier is unchanged, and its normalized profile has the same uniform weighted-translation bounds as the synthesizing profile.

  1. def OAI.LipschitzHilbert.PacketRepresentation.reflectedConjugateProfile line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reflectedConjugateProfile_apply line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.reflectedConjugateProfile_weightedTranslate line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.physical_reflectedConjugateProfile line 29
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.physical_analyzing_packet line 44
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.scaled_analyzing_profile_bound line 54