TopNeighborhood.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform vertical neighborhoods for an entire family of sums, with one measurable exceptional set and an explicit area moment bound.