OAI/Geometry/SmoothYau/Spectrum/CoordinateMetricLaplacianGerm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.coordinateMetricLaplacian_germ line 45
2. lemma OAI.YauCounterexamples.coordinateMetricLaplacian_zero line 59
3. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_self_germ line 63
4. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_self_zero line 72
5. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_residual_tsupport line 78
6. lemma OAI.YauCounterexamples.canonicalCutoffWave_tsupport line 92
7. lemma OAI.YauCounterexamples.canonicalCutoffWave_compact line 99
8. lemma OAI.YauCounterexamples.normalChartWave_tsupport line 106
9. lemma OAI.YauCounterexamples.normalChartWave_germ line 121