OAI/Analysis/LipschitzHilbert/Packets/FiniteNormalizedPacketLattice.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Realization of an arbitrary finite part of the translated lattice by the actual normalized packet data. The site fibers are shared by all carrier components and add no extra terms.

  1. def OAI.LipschitzHilbert.PacketRepresentation.finiteSiteFiber line 25
  2. def OAI.LipschitzHilbert.PacketRepresentation.finiteSiteFiberEquiv line 28
  3. def OAI.LipschitzHilbert.PacketRepresentation.finiteNormalizedPacketLattice line 34
  4. def OAI.LipschitzHilbert.PacketRepresentation.finiteNormalizedPacketEquiv line 44
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteNormalizedPacketEquiv_apply line 49
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteNormalizedPacket_sum line 54