OAI/Geometry/SmoothYau/Spectrum/PinningFactorGradient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.laplaceBeltrami_congr_nhds line 20
2. lemma OAI.YauCounterexamples.laplaceBeltrami_tsupport line 42
3. lemma OAI.YauCounterexamples.laplaceResidual_tsupport line 52
4. theorem OAI.YauCounterexamples.compact_chart_weighted_jet_transfer line 60
5. lemma OAI.YauCounterexamples.pinning_factor_squared line 91
6. lemma OAI.YauCounterexamples.chart_germ_of_pullback line 122
7. theorem OAI.YauCounterexamples.local_eigen_proportional_of_annular_rank line 134
8. lemma OAI.YauCounterexamples.pinning_factor_gradient line 223
9. theorem OAI.YauCounterexamples.local_eigen_proportional_of_gradient_rank line 246