OAI/Analysis/LipschitzHilbert/Trees/SourceOrdinaryAdjoint.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.SourceLabeledLattice.ordinaryForwardSum line 16
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryAdjointSum line 22
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.masked_physical_packet_memLp line 27
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryAdjointSum_memLp line 41
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinary_forward_pairing line 47
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinary_adjoint_pairing line 79
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinary_forward_adjoint_pairing line 96