OAI/Analysis/LipschitzHilbert/Estimates/ThinTopTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted tail for actual thin clipped tops, with geometric admissibility and indicator averages discharged. The remaining data are exactly the top witnesses, their density and slope agreement, and the published Lacey--Li estimate.

  1. theorem OAI.LipschitzHilbert.thin_top_weighted_tail line 16