OAI/Analysis/LipschitzHilbert/Estimates/MixedTopTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A mixed family of clipped tops is split by aspect ratio. Both pieces use the same published Lacey--Li input, and the resulting constant is uniform in the finite family and dilation.

  1. theorem OAI.LipschitzHilbert.mixed_top_weighted_tail line 15