OAI/Analysis/LipschitzHilbert/Estimates/SharpHilbertThird.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The third-moment bound, including bounded measurable inputs needed as explicit dual test functions.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpHilbert_two_four_constants line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpHilbert_uniform_third_bounded line 34