OAI/Analysis/LipschitzHilbert/Estimates/ShortL2Operator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The preliminary L2 realization of the short-time operator. Its logarithmic kernel norm is used only for continuity and density.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_schwartz_add line 15
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_schwartz_smul line 23
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSchwartz_memLp line 32
  4. def OAI.LipschitzHilbert.PacketRepresentation.shortSchwartzToL2 line 37
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSchwartzToL2_norm line 61
  6. def OAI.LipschitzHilbert.PacketRepresentation.shortL2Operator line 77
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.shortL2Operator_onSchwartz line 82
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.shortL2Operator_norm line 89