OAI/Analysis/LipschitzHilbert/Estimates/ShortSlopeLp.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The continuous short-time operator agrees on every L2 class with its integral representative. This permits exact support localization.

  1. def OAI.LipschitzHilbert.PacketRepresentation.shortSample line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSample_measurable line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSample_energy line 21
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSample_congr_ae line 32
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_congr_ae line 46
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_integrand_ae line 68
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_sub_ae line 98