OAI/Analysis/LipschitzHilbert/Estimates/NormalizedLatticeSpectrum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal normalized finite lattices inherit the frequency strip, positive annulus, and carrier bin from their fixed Fourier plateaus.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.normalizedPacketLattice_spectrum line 33
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.normalizedAnalysisFamily_spectrum line 61