OAI/Analysis/LipschitzHilbert/Packets/NormalizedPacketLattice.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual Fourier-separated synthesis profiles on arbitrary finite translated lattices. The slopes have no global shear restriction.

  1. def OAI.LipschitzHilbert.PacketRepresentation.normalizedPacketLattice line 25

    Source documentation

    All carrier components share each actual site. The profile bound comes from the single normalized profile, independently of these data.

    def normalizedPacketLattice : PacketLatticeData N κ Label Item where
…

    Mentions: OAI.LipschitzHilbert.PacketLatticeData

  2. theorem OAI.LipschitzHilbert.PacketRepresentation.normalizedPacketLattice_synthesis line 51
  3. def OAI.LipschitzHilbert.PacketRepresentation.normalizedAnalysisFamily line 65
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.normalizedAnalysisFamily_bound line 69
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.normalizedAnalysisFamily_packet line 78