OAI/Analysis/LipschitzHilbert/Fourier/FrequencyProfileNormalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

In the packet coordinates the two Fourier modulations are just weighted translations of the unmodulated profile. The vertical carrier phase cancels exactly.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.packetCoordinates_symm_apply line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.weightedTranslatedProfile_apply line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.horizontalFrequencyProfile_eq line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalFrequencyProfile_eq line 39