OAI/Analysis/LipschitzHilbert/Estimates/HilbertFiniteL2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform L2 bounds for the actual finite smooth Hilbert convolutions.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel_unit line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertFinite_kernel line 19
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertFinite_L2 line 35