OAI/Analysis/LipschitzHilbert/Packets/PacketConvolution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The continuous packet identity in §2, with the actual convolution kernels and the exact area normalization. Absolute integrability follows from L1 kernels and input and a bounded measurable test.

  1. abbrev OAI.LipschitzHilbert.PacketRepresentation.planeMeasure line 16
  2. def OAI.LipschitzHilbert.PacketRepresentation.kernelConvolution line 18
  3. def OAI.LipschitzHilbert.PacketRepresentation.analyzingWave line 21
  4. def OAI.LipschitzHilbert.PacketRepresentation.synthesisWave line 24
  5. def OAI.LipschitzHilbert.PacketRepresentation.coefficient line 27
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.coefficient_eq line 30
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.kernelConvolution_integrable line 39
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.weighted_convolution_integrable line 44
  9. def OAI.LipschitzHilbert.PacketRepresentation.packetProduct line 57
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.packetProduct_eq line 61
  11. theorem OAI.LipschitzHilbert.PacketRepresentation.packetProduct_integrable line 71
  12. theorem OAI.LipschitzHilbert.PacketRepresentation.continuous_packet_identity line 82