OAI/Analysis/LipschitzHilbert/Estimates/HilbertSignFourth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fourth-power bound for the sign multiplier on Schwartz functions.

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