OAI/Analysis/LipschitzHilbert/Estimates/HilbertFiniteFourth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform fourth-power bounds for the finite smooth Hilbert kernel.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertFinite_fourth line 13