OAI/Analysis/LipschitzHilbert/Estimates/TopDilationTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Scaling the mixed rectangle bound by the actual top area gives a quadratic distribution bound. The density loses exactly two powers of the dilation radius, which will give a cubic testing cost.

  1. theorem OAI.LipschitzHilbert.top_dilation_square_tail line 14