OAI/Analysis/LipschitzHilbert/Packets/PacketDataAdjoint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Literal finite adjoint duality for the ordinary masked packets.

  1. def OAI.LipschitzHilbert.PacketLatticeData.ordinaryForwardSum line 17
  2. def OAI.LipschitzHilbert.PacketLatticeData.ordinaryAdjointSum line 23
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.masked_physical_packet_memLp line 28
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.ordinaryAdjointSum_memLp line 42
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.ordinary_forward_pairing line 48
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.ordinary_adjoint_pairing line 80
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.ordinary_forward_adjoint_pairing line 97