OAI/Analysis/LipschitzHilbert/Fourier/VerticalBinProfile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A fixed real smooth bin profile whose squared translates sum to one. The trigonometric construction avoids a variable normalization denominator.

  1. def OAI.LipschitzHilbert.PacketRepresentation.binSquareStep line 13
  2. def OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfileReal line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.binSquareStep_zero line 18
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.binSquareStep_one line 21
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfileReal_sq line 24
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfileReal_zero line 34
  7. def OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfile line 39
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfile_apply line 55
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfile_real line 57
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfile_support line 60
  11. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfileReal_sum_sq line 71
  12. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfile_sum_sq line 82