OAI/Geometry/SmoothYau/Estimates/ActualRadialCorrugationStrict.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.YauCounterexamples.cutoff_small_product_boundline 20 - theorem
OAI.YauCounterexamples.corrugationSecondRemainder_small_productline 42 - theorem
OAI.YauCounterexamples.corrugationSecondRemainder_small_product_scaledline 78 - theorem
OAI.YauCounterexamples.actual_radialCorrugation_strictline 144