OAI/Analysis/LipschitzHilbert/Estimates/HilbertSharpPairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform comparison of the actual sharp Hilbert pairing with its finite annular decomposition, with a restricted mass gain at both endpoints.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertSharp_pairing_error line 12