OAI/Geometry/SmoothYau/Spectrum/ContinuousEigenpairLinearization.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.compact_eigenspace_finite line 21
2. structure OAI.YauCounterexamples.PositivePairing line 30
3. def OAI.YauCounterexamples.PositivePairing.perpendicular line 38
4. instance OAI.YauCounterexamples.PositivePairing.perpendicular_complete line 40
5. lemma OAI.YauCounterexamples.PositivePairing.perpendicular_invariant line 44
6. theorem OAI.YauCounterexamples.PositivePairing.simple_eigenvalue_complement_invertible line 53
7. def OAI.YauCounterexamples.CompactMetricAtlas.realRepresentative line 102
8. lemma OAI.YauCounterexamples.CompactMetricAtlas.realRepresentative_apply line 106
9. lemma OAI.YauCounterexamples.CompactMetricAtlas.realRepresentative_injective line 110
10. def OAI.YauCounterexamples.CompactMetricAtlas.intrinsicForm line 121
11. lemma OAI.YauCounterexamples.CompactMetricAtlas.intrinsicForm_apply line 127
12. def OAI.YauCounterexamples.CompactMetricAtlas.intrinsicPairing line 131
13. def OAI.YauCounterexamples.CompactMetricAtlas.realSpectralResolvent line 157
14. lemma OAI.YauCounterexamples.CompactMetricAtlas.realSpectralResolvent_compact line 162
15. lemma OAI.YauCounterexamples.MetricIntegralAtlas.mean_sub line 194
16. lemma OAI.YauCounterexamples.MetricIntegralAtlas.mean_const_mul line 201
17. theorem OAI.YauCounterexamples.CompactMetricAtlas.realSpectralResolvent_symmetric line 211
18. def OAI.YauCounterexamples.PositivePairing.eigenpairLinearization line 263
19. lemma OAI.YauCounterexamples.PositivePairing.eigenpairLinearization_apply line 270
20. lemma OAI.YauCounterexamples.PositivePairing.eigenpairLinearization_bijective line 273
21. abbrev OAI.YauCounterexamples.PositivePairing.EigenpairParameters line 321
22. def OAI.YauCounterexamples.PositivePairing.eigenpairMap line 323
23. def OAI.YauCounterexamples.PositivePairing.eigenpairDerivative line 326
24. lemma OAI.YauCounterexamples.PositivePairing.eigenpairDerivative_apply line 335
25. lemma OAI.YauCounterexamples.PositivePairing.eigenpairDerivative_bijective line 341
26. lemma OAI.YauCounterexamples.PositivePairing.eigenpairMap_hasStrictFDerivAt line 369
27. theorem OAI.YauCounterexamples.PositivePairing.simple_eigenpair_persistence line 383
28. lemma OAI.YauCounterexamples.PositivePairing.continuous_eigenpairLinearization line 435
29. lemma OAI.YauCounterexamples.PositivePairing.simple_of_linearization_injective line 453
30. lemma OAI.YauCounterexamples.PositivePairing.eigenpair_linearization_units_eventually line 472
31. theorem OAI.YauCounterexamples.PositivePairing.simple_eigenpair_persistence_with_simplicity line 484