OAI/Analysis/LipschitzHilbert/Estimates/NeighborhoodGeometric.lean
2 declarations, 0 contain sorry, 0 declared as axioms
A common vertical-neighborhood exceptional set has exponentially small area when the chosen even line moment has polynomial growth.
- theorem
OAI.LipschitzHilbert.quarter_area_of_even_momentline 15 - theorem
OAI.LipschitzHilbert.top_neighborhood_geometricline 41