OAI/Geometry/SmoothYau/Estimates/LocalZeroAcrossLevel.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.YauCounterexamples.exponential_square_integrableline 15 - lemma
OAI.YauCounterexamples.exponential_square_integralline 24 - lemma
OAI.YauCounterexamples.exponential_square_lowerline 34 - lemma
OAI.YauCounterexamples.exponential_square_upperline 53 - theorem
OAI.YauCounterexamples.exponential_support_dominanceline 68 - theorem
OAI.YauCounterexamples.local_zero_across_levelline 115