OAI/Analysis/LipschitzHilbert/Estimates/GlobalNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global top concentration from uniform local line moments. Box exceptions are constructed by the proved vertical Sobolev estimate, and their areas are summed over the whole plane.

  1. theorem OAI.LipschitzHilbert.global_top_neighborhood line 16