OAI/Geometry/SmoothYau/DifferentialEq/ExistsMetricSignQuasimodesSubregions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.exp_profile_log_derivative line 50
2. lemma OAI.YauCounterexamples.finiteWaveSuperposition_compact line 60
3. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_finiteWaveSum_uniform line 75
4. theorem OAI.YauCounterexamples.exists_compact_metric_quasimodes line 93
5. theorem OAI.YauCounterexamples.exists_metric_sign_quasimodes_supported line 196
6. theorem OAI.YauCounterexamples.exists_metric_sign_quasimodes_subregions_supported line 308