OAI/Analysis/LipschitzHilbert/Geometry/PacketDataReferenceSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A finite portion of an unrestricted packet family inside a reference cone embeds into the bounded reference lattice without changing a wave. This is the bridge used after a density keeper has been selected.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.reference_bounds_of_density_cell line 19
  2. def OAI.LipschitzHilbert.PacketLatticeData.referencePacket line 41
  3. def OAI.LipschitzHilbert.PacketLatticeData.originalPacket line 48
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.original_referencePacket line 51
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.referencePacket_physical line 58
  6. def OAI.LipschitzHilbert.PacketLatticeData.referencePacketEmbedding line 75
  7. def OAI.LipschitzHilbert.PacketLatticeData.referencePackets line 85
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.referencePackets_sum line 89