OAI/Analysis/LipschitzHilbert/Fourier/KernelDifferencePairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A kernel L1 error controls the actual localized bilinear form by the smaller of the input and test masses.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.slope_integrand_integrable line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.slopeOperator_kernel_sub line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_kernel_sub line 29
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.kernelDifference_pairing line 43