OAI/Geometry/SmoothYau/Smoothness/FiniteAmplitudeCentralBound.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.YauCounterexamples.smoothFiniteWave_at_zeroline 45 - lemma
OAI.YauCounterexamples.smoothFiniteWave_central_derivativeline 50 - lemma
OAI.YauCounterexamples.smoothFiniteWave_cutoff_germline 67 - theorem
OAI.YauCounterexamples.canonicalCutoffWave_central_jetline 75 - lemma
OAI.YauCounterexamples.finite_amplitude_central_boundline 154 - lemma
OAI.YauCounterexamples.normalize_central_derivativeline 177 - theorem
OAI.YauCounterexamples.generated_waves_central_errorline 186