OAI/Analysis/LipschitzHilbert/Packets/PacketDataReferenceCross.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local reference restriction preserves the actual two-profile packet operator, including its masked analyzing coefficient.

  1. abbrev OAI.LipschitzHilbert.PacketLatticeData.referenceAlt line 18
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceAlt_bound line 23
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceAlt_physicalPacket line 32
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_crossPacketValue line 45